재귀

Question

나는 dfold를 사용하려고

없이 함수 n 번을 호출하기 위해, 유형이 각 반복 함수 호출 후 변경할 수있는 배를 만들기 here

dfold 
    :: KnownNat k  
    => Proxy (p :: TyFun Nat * -> *)  
    -> (forall l. SNat l -> a -> (p @@ l) -> p @@ (l + 1)) 
    -> (p @@ 0) 
    -> Vec k a 
    -> p @@ k 

를 정의 기본적으로이 배는 그 매 사이클마다 새로운 유형을 반환 할 수 있습니다. 에

bitonicSort 
    :: forall n a. (KnownNat n, Ord a) 
    => (Vec n a -> Vec n a)    --^The recursive step 
    -> (Vec (2 * n) a -> Vec (2 * n) a) --^Merge step 
    -> Vec (2 * n) a     --^Input vector 
    -> Vec (2 * n) a     --^Output vector 
bitonicMerge 
    :: forall n a. (Ord a , KnownNat n) 
    => (Vec n a -> Vec n a) --^The recursive step 
    -> Vec (2 * n) a  --^Input vector 
    -> Vec (2 * n) a  --^Output vector 

예제를 사용 : 함께 dfold 생성하는 유형의 중요한 https://github.com/adamwalker/clash-utils/blob/master/src/CLaSH/Sort.hs

나는 두 가지 기능 :이 프로젝트에 정의 된 bitonicSort을 일반화하려고

위에 언급 된 프로젝트는 다음과 같습니다.

bitonicSorterExample 
    :: forall a. (Ord a) 
    => Vec 16 a --^Input vector 
    -> Vec 16 a --^Sorted output vector 
bitonicSorterExample = sort16 
    where 
    sort16 = bitonicSort sort8 merge16 
    merge16 = bitonicMerge merge8 

    sort8 = bitonicSort sort4 merge8 
    merge8 = bitonicMerge merge4 

    sort4 = bitonicSort sort2 merge4 
    merge4 = bitonicMerge merge2 

    sort2 = bitonicSort id merge2 
    merge2 = bitonicMerge id 

d는보다 일반적인 버전을 만들었습니다. 지정된 크기의 벡터와 작품에

bSort16 :: Ord a => Vec 16 a -> Vec 16 a 
bSort16 = fst $ genBitonic $ genBitonic $ genBitonic $ genBitonic bitonicBase 

bSort8 :: Ord a => Vec 8 a -> Vec 8 a 
bSort8 = fst $ genBitonic $ genBitonic $ genBitonic bitonicBase 

bSort4 :: Ord a => Vec 4 a -> Vec 4 a 
bSort4 = fst $ genBitonic $ genBitonic bitonicBase 

bSort2 :: Ord a => Vec 2 a -> Vec 2 a 
bSort2 = fst $ genBitonic bitonicBase 

각 정렬 : 나는 빠른과 같이 새로운 바이 토닉 정렬을 할 수 있습니다이 버전으로

genBitonic :: (Ord a, KnownNat n) => 
    (Vec n a -> Vec n a, Vec (2 * n) a -> Vec (2 * n) a) 
    -> (Vec (2 * n) a -> Vec (2 * n) a, Vec (4 * n) a -> Vec (4 * n) a) 
genBitonic (bSort,bMerge) = (bitonicSort bSort bMerge, bitonicMerge bMerge) 

bitonicBase :: Ord a => (Vec 1 a -> Vec 1 a, Vec 2 a -> Vec 2 a) 
bitonicBase = (id, bitonicMerge id) 

.

testVec16 :: Num a => Vec 16 a 
testVec16 = 9 :> 2 :> 8 :> 6 :> 3 :> 7 :> 0 :> 1 :> 4 :> 5 :> 2 :> 8 :> 6 :> 3 :> 7 :> 0 :> Nil 

testVec8 :: Num a => Vec 8 a 
testVec8 = 9 :> 2 :> 8 :> 6 :> 3 :> 7 :> 0 :> 1 :> Nil 

testVec4 :: Num a => Vec 4 a 
testVec4 = 9 :> 2 :> 8 :> 6 :> Nil 

testVec2 :: Num a => Vec 2 a 
testVec2 = 2 :> 9 :> Nil 

빠른 노트 : 제가 적용 "genBitonic"을 "bitonicBase"t 시간에 노력하고

• .

• 내가 VHDL이 종합하는 충돌을 사용하고, 그래서 적용 재귀를 사용할 수 없습니다 t 시간

• 우리는 항상 같은 크기의 VEC에있는 VEC 크기가 2^t 정렬됩니다

• 는 "VEC NA는"크기 N의 벡터이고, I는 주어진 VEC위한 함수를 생성하는 기능을하고 싶은

입력. dfold 또는 dtfold를 사용하는 것이 올바른 경로라고 생각합니다.

genBitonic과 같은 형식으로 폴드하고 싶었습니다.

그런 다음 fst을 사용하여 정렬에 필요한 기능을 얻으십시오.

한 : 그 기반을 소요하는 기능을 얻을 수 조성물을 사용하여 접어

나는 두 가지 디자인을했다.

bSort8 :: Ord a => Vec 8 a -> Vec 8 a 
bSort8 = fst $ genBitonic.genBitonic.genBitonic $ bitonicBase 

이

**If composition was performed three times** 

foo3 :: 
    (Ord a, KnownNat n) => 
    (Vec n a -> Vec n a, Vec (2 * n) a -> Vec (2 * n) a) 
    -> (Vec (2 * (2 * (2 * n))) a -> Vec (2 * (2 * (2 * n))) a, 
     Vec (4 * (2 * (2 * n))) a -> Vec (4 * (2 * (2 * n))) a) 

두 같은 것을 이어질 것베이스 대답되기 전에 : 제 생각에 축적을 시작하는 b 값으로 bitonicBase을 사용하는 것이 었습니다. 이는 fst을 적용하기 전에 내가 필요로하는 형태로 직접 작성되었을 것입니다.

편집 vecAcum은 바로 dfold의 내부에 구축 값이 될하기위한 것입니다. dfold 예에서

그들은 목록 연산자의 바로 벡터 형태 인 :>를 사용하여 접어서 :

>>> :t (:>) 
(:>) :: a -> Vec n a -> Vec (n + 1) a 

내가하고 싶은 것은 같은 두 가지 기능의 튜플 걸릴 수 있습니다 :

genBitonic :: (Ord a, KnownNat n) => 
    (Vec n a -> Vec n a, Vec (2 * n) a -> Vec (2 * n) a) 
    -> (Vec (2 * n) a -> Vec (2 * n) a, Vec (4 * n) a -> Vec (4 * n) a) 

을

그리고 작성하십시오.

(Vec n a -> Vec n a, Vec (2 * n) a -> Vec (2 * n) a) 
-> (Vec (2 * (2 * n)) a -> Vec (2 * (2 * n)) a, Vec (4 * (2 * n)) a -> Vec (4 * (2 * n)) a) 

그래서 다음 기본 기능 유형을 굳은 것 같습니다 그래서 genBitonic . genBitonic 유형있을 것입니다. 예 :

bitonicBase :: Ord a => (Vec 1 a -> Vec 1 a, Vec 2 a -> Vec 2 a) 
bitonicBase = (id, bitonicMerge id) 
bSort4 :: Ord a => Vec 4 a -> Vec 4 a 
bSort4 = fst $ genBitonic $ genBitonic bitonicBase 

나는 길이 n의 벡터에 재귀를 수행하는 것과 같습니다 길이 n의 벡터에 대한 기능을 구축하기 위해 dfold을 사용하고 있습니다.

내가 시도 :

내가

data SplitHalf (a :: *) (f :: TyFun Nat *) :: * 
type instance Apply (SplitHalf a) l = (Vec (2^l) a -> Vec (2^l) a, Vec (2^(l + 1)) a -> Vec (2^(l + 1)) a) 

generateBitonicSortN2 :: forall k a . (Ord a, KnownNat k) => SNat k -> Vec (2^k) a -> Vec (2^k) a 
generateBitonicSortN2 k = fst $ dfold (Proxy :: Proxy (SplitHalf a)) vecAcum base vecMath 
    where 
    vecMath = operationList k 


vecAcum :: (KnownNat l, KnownNat gl, Ord a) => SNat l 
           -> (SNat gl -> SplitHalf a @@ gl -> SplitHalf a @@ (gl+1)) 
           -> SplitHalf a @@ l 
           -> SplitHalf a @@ (l+1) 
vecAcum l0 f acc = undefined -- (f l0) acc 

base :: (Ord a) => SplitHalf a @@ 0 
base = (id,id) 

general :: (KnownNat l, Ord a) 
     => SNat l 
     -> SplitHalf a @@ l 
     -> SplitHalf a @@ (l+1) 
general _ (x,y) = (bitonicSort x y, bitonicMerge y) 

operationList :: (KnownNat k, KnownNat l, Ord a) 
       => SNat k 
       -> Vec k 
        (SNat l 
       -> SplitHalf a @@ l 
       -> SplitHalf a @@ (l+1)) 
operationList k0 = replicate k0 general 

내가 확장에게 dfold 소스 코드를 사용하고

이

{-# LANGUAGE BangPatterns   #-} 
{-# LANGUAGE DataKinds   #-} 
{-# LANGUAGE GADTs    #-} 
{-# LANGUAGE KindSignatures  #-} 
{-# LANGUAGE MagicHash   #-} 
{-# LANGUAGE PatternSynonyms  #-} 
{-# LANGUAGE Rank2Types   #-} 
{-# LANGUAGE ScopedTypeVariables #-} 
{-# LANGUAGE TemplateHaskell  #-} 
{-# LANGUAGE TupleSections  #-} 
{-# LANGUAGE TypeApplications  #-} 
{-# LANGUAGE TypeFamilies   #-} 
{-# LANGUAGE TypeOperators  #-} 
{-# LANGUAGE UndecidableInstances #-} 
{-# LANGUAGE ViewPatterns   #-} 

{-# LANGUAGE Trustworthy #-} 

오류 메시지를 사용 dfold 아래에 나열된 모범을 따르려고 노력 :

Sort.hs:182:71: error: 
    * Could not deduce (KnownNat l) arising from a use of `vecAcum' 
     from the context: (Ord a, KnownNat k) 
     bound by the type signature for: 
        generateBitonicSortN2 :: (Ord a, KnownNat k) => 
              SNat k -> Vec (2^k) a -> Vec (2^k) a 
     at Sort.hs:181:1-98 
     Possible fix: 
     add (KnownNat l) to the context of 
      a type expected by the context: 
      SNat l 
      -> (SNat l0 
       -> (Vec (2^l0) a -> Vec (2^l0) a, 
        Vec (2^(l0 + 1)) a -> Vec (2^(l0 + 1)) a) 
       -> (Vec (2^(l0 + 1)) a -> Vec (2^(l0 + 1)) a, 
        Vec (2^((l0 + 1) + 1)) a -> Vec (2^((l0 + 1) + 1)) a)) 
      -> SplitHalf a @@ l 
      -> SplitHalf a @@ (l + 1) 
    * In the second argument of `dfold', namely `vecAcum' 
     In the second argument of `($)', namely 
     `dfold (Proxy :: Proxy (SplitHalf a)) vecAcum base vecMath' 
     In the expression: 
     fst $ dfold (Proxy :: Proxy (SplitHalf a)) vecAcum base vecMath 

Sort.hs:182:84: error: 
    * Could not deduce (KnownNat l0) arising from a use of `vecMath' 
     from the context: (Ord a, KnownNat k) 
     bound by the type signature for: 
        generateBitonicSortN2 :: (Ord a, KnownNat k) => 
              SNat k -> Vec (2^k) a -> Vec (2^k) a 
     at Sort.hs:181:1-98 
     The type variable `l0' is ambiguous 
    * In the fourth argument of `dfold', namely `vecMath' 
     In the second argument of `($)', namely 
     `dfold (Proxy :: Proxy (SplitHalf a)) vecAcum base vecMath' 
     In the expression: 
     fst $ dfold (Proxy :: Proxy (SplitHalf a)) vecAcum base vecMath 
Failed, modules loaded: none. 

** 편집 ** 훨씬 자세히 추가되었습니다.

Answer 1

base 사례가 잘못되었습니다. 그것은

base :: (Ord a) => SplitHalf a @@ 0 
base = (id, bitonicMerge id) 

여기 GHC 8.0.2 테스트 완전히 작업 버전이, (하지만이 GHC 8.0.2 기반의 충돌에서 모두 같은 작업을해야이다, 모두 함께 퍼팅 할 것을 Prelude 수입 물건을 모듈로한다). operationList 척추를 제외하고는 사용되지 않으므로 대신 Vec n()을 사용할 수 있습니다.

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-} 
{-# LANGUAGE Rank2Types, ScopedTypeVariables #-} 
{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances #-} 

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise -fplugin GHC.TypeLits.KnownNat.Solver #-} 
{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-redundant-constraints #-} 

{-# LANGUAGE NoImplicitPrelude #-} 
import Prelude (Integer, (+), Num, ($), undefined, id, fst, Int, otherwise) 
import CLaSH.Sized.Vector 
import CLaSH.Promoted.Nat 
import Data.Singletons 
import GHC.TypeLits 
import Data.Ord 

type ExpVec k a = Vec (2^k) a 

data SplitHalf (a :: *) (f :: TyFun Nat *) :: * 
type instance Apply (SplitHalf a) k = (ExpVec k a -> ExpVec k a, ExpVec (k + 1) a -> ExpVec (k + 1) a) 

generateBitonicSortN2 :: forall k a . (Ord a, KnownNat k) => SNat k -> ExpVec k a -> ExpVec k a 
generateBitonicSortN2 k = fst $ dfold (Proxy :: Proxy (SplitHalf a)) step base (replicate k()) 
    where 
    step :: SNat l ->() -> SplitHalf a @@ l -> SplitHalf a @@ (l+1) 
    step SNat _ (sort, merge) = (bitonicSort sort merge, bitonicMerge merge) 

    base = (id, bitonicMerge id) 

예상대로 작동합니다.:

*Main> generateBitonicSortN2 (snatProxy Proxy) testVec2 
<9,2> 
*Main> generateBitonicSortN2 (snatProxy Proxy) testVec4 
<9,8,6,2> 
*Main> generateBitonicSortN2 (snatProxy Proxy) testVec8 
<9,8,7,6,3,2,1,0> 
*Main> generateBitonicSortN2 (snatProxy Proxy) testVec16 
<9,8,8,7,7,6,6,5,4,3,3,2,2,1,0,0> 
*Main> 

Answer 2

내가 VHDL이 종합하는 충돌을 사용하고, 그래서 t 시간을 적용하는 재귀를 사용할 수는

나는이 문장을 이해하지만, 그 이외하지 않습니다

{-# LANGUAGE GADTs, DataKinds, TypeFamilies, UndecidableInstances, 
     FlexibleInstances, FlexibleContexts, ConstraintKinds, 
     UndecidableSuperClasses, TypeOperators #-} 

import GHC.TypeLits 
import GHC.Exts (Constraint) 
import Data.Proxy 

data Peano = Z | S Peano 

data SPeano n where 
    SZ :: SPeano Z 
    SS :: SPeano n -> SPeano (S n) 

type family PowerOfTwo p where 
    PowerOfTwo Z = 1 
    PowerOfTwo (S p) = 2 * PowerOfTwo p 

type family KnownPowersOfTwo p :: Constraint where 
    KnownPowersOfTwo Z =() 
    KnownPowersOfTwo (S p) = (KnownNat (PowerOfTwo p), KnownPowersOfTwo p) 

data Vec (n :: Nat) a -- abstract 

type OnVec n a = Vec n a -> Vec n a 
type GenBitonic n a = (OnVec n a, OnVec (2 * n) a) 

genBitonic :: (Ord a, KnownNat n) => GenBitonic n a -> GenBitonic (2 * n) a 
genBitonic = undefined 

bitonicBase :: Ord a => GenBitonic 1 a 
bitonicBase = undefined 

genBitonicN :: (Ord a, KnownPowersOfTwo p) => SPeano p -> GenBitonic (PowerOfTwo p) a 
genBitonicN SZ = bitonicBase 
genBitonicN (SS p) = genBitonic (genBitonicN p) 

genBitonicN은 힘을 나타내는 피아노 수에 대한 재귀에 의해 정의됩니다. 각 재귀 단계에서 새로운 KnownNat (PowerOfTwo p)이 나타납니다 (KnownPowersOfTwo 유형 패밀리를 통해). 가치 레벨 genBitonicN에서 하찮은이며 원하는대로. 그러나 우리는 편리한 bSortN을 정의하기 위해 몇 가지 추가 장비가 필요합니다 : 여기

type family Lit n where 
    Lit 0 = Z 
    Lit n = S (Lit (n - 1)) 

class IPeano n where 
    speano :: SPeano n 

instance IPeano Z where 
    speano = SZ 

instance IPeano n => IPeano (S n) where 
    speano = SS speano 

class (n ~ PowerOfTwo (PowerOf n), KnownPowersOfTwo (PowerOf n)) => 
     IsPowerOfTwo n where 
    type PowerOf n :: Peano 
    getPower :: SPeano (PowerOf n) 

instance IsPowerOfTwo 1 where 
    type PowerOf 1 = Lit 0 
    getPower = speano 

instance IsPowerOfTwo 2 where 
    type PowerOf 2 = Lit 1 
    getPower = speano 

instance IsPowerOfTwo 4 where 
    type PowerOf 4 = Lit 2 
    getPower = speano 

instance IsPowerOfTwo 8 where 
    type PowerOf 8 = Lit 3 
    getPower = speano 

instance IsPowerOfTwo 16 where 
    type PowerOf 16 = Lit 4 
    getPower = speano 

-- more powers go here 

bSortN :: (IsPowerOfTwo n, Ord a) => OnVec n a 
bSortN = fst $ genBitonicN getPower 

은 몇 가지 예입니다 :

bSort1 :: Ord a => OnVec 1 a 
bSort1 = bSortN 

bSort2 :: Ord a => OnVec 2 a 
bSort2 = bSortN 

bSort4 :: Ord a => OnVec 4 a 
bSort4 = bSortN 

bSort8 :: Ord a => OnVec 8 a 
bSort8 = bSortN 

bSort16 :: Ord a => OnVec 16 a 
bSort16 = bSortN 

나는 우리가 두 가지의 각 전원에 대한 IsPowerOfTwo을 정의 피할 수 있는지 여부를 알 수 없습니다.

업데이트 :

pnatToSPeano :: IPeano (Lit n) => proxy n -> SPeano (Lit n) 
pnatToSPeano _ = speano 

bSortNP :: (IPeano (Lit p), KnownPowersOfTwo (Lit p), Ord a) 
     => proxy p -> OnVec (PowerOfTwo (Lit p)) a 
bSortNP = fst . genBitonicN . pnatToSPeano 

예 :

bSort16 :: Ord a => OnVec 16 a 
bSort16 = bSortNP (Proxy :: Proxy 4)