Tworzenie fałd, który pozwala typ zmieniać po każdym wielokrotnego wywołania funkcji w celu wywołania funkcji n razy bez rekursji

Question

Próbuję użyć dfold zdefiniowane 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 

Zasadniczo jest to fałd że pozwala na zwrócenie nowego typu po każdym cyklu.

Staram się uogólnić bitonicSort zdefiniowane w tym projekcie: https://github.com/adamwalker/clash-utils/blob/master/src/CLaSH/Sort.hs

I dwie funkcje, które są ważne dla typów że dfold z generują:

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 

Przykład używany w wspomniany wyżej projekt to:

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 

Poszedłem d zrobił bardziej ogólną wersję.

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) 

W tej wersji można szybko zrobić nowe rodzaje Bitonic tak:

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 

Każdy Sortuj z pracy z wektorem określonym rozmiarze.

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 

Szybkie notatki:

• Próbuję Zastosuj "genBitonic" na "bitonicBase" t razy.

• używam starcia do syntezy do VHDL, więc nie mogę użyć rekurencji do zastosowania t razy

• zawsze będziemy sortowania VEC wielkość 2^tw do vec tej samej wielkości

• „vec nA” oznacza wektor wielkości n i wpisać

chciałbym do funkcji, która generuje funkcji dla danej Vec. Wierzę, że przy użyciu dfold lub dtfold, jest poprawna ścieżka tutaj.

Chciałam złożyć coś podobnego do funkcji genBitonic.

Następnie użyj fst, aby uzyskać funkcję potrzebną do sortowania.

miałem dwa możliwe wzory:

Jeden: krotnie stosując kompozycję, aby funkcja, która, która przyjmuje zasadę.

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

Przed zasadę odpowiedział byłoby zaowocowały czymś jak

**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) 

Dwa: Drugi pomysł był użyć bitonicBase jako wartość b, aby rozpocząć gromadzenie się dalej. Spowodowałoby to bezpośrednio formę, której potrzebuję, zanim zgłoszę fst.

Edit vecAcum właśnie ma być wartość budowania wewnątrz dfold.

W dfold przykład oni krotnie stosując :> który jest po prostu formą wektor operatora lista :

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

Co chcę zrobić, to wziąć krotki dwóch funkcji, takich jak:

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) 

I skomponuj je. Więc genBitonic . genBitonic musiałby typ:

(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) 

Więc funkcja bazowa byłaby co krzepnie typy. np.

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 

Używam dfold zbudować funkcję dla wektorów o długości n, który jest odpowiednikiem robi rekursji na wektorem o długości n.

Próbowałem:

starałem się naśladować przykład uszeregowane pod 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 

używam rozszerzeń kodu źródłowego dfold wykorzystuje

{-# 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 #-} 

komunikatów o błędach:

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. 

** EDYTUJ ** Dodano znacznie więcej szczegółów.

Answer 1

Wasz przypadek base był nieprawidłowy; powinno być

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

Kładzenie to wszystko razem, oto wersja w pełni działa, testowany na GHC 8.0.2 (ale to powinno działać wszystko jedno na zderzenie GHC 8.0.2 opartej na modulo rzeczy Prelude import). Okazuje się, że rzecz nie jest używana z wyjątkiem kręgosłupa, dlatego możemy użyć zamiast tego 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) 

Działa zgodnie z oczekiwaniami, np.:

*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

używam starcia do syntezy do VHDL, więc nie mogę użyć rekurencji do zastosowania t razy

Nie rozumiem to zdanie, ale poza tym:

{-# 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 definiuje się przez rekursję na numerze peano, który reprezentuje moc. Na każdym etapie rekursywnym pojawia się nowy KnownNat (PowerOfTwo p) (poprzez rodzinę typu KnownPowersOfTwo). Na poziomie wartości genBitonicN jest trywialny i po prostu robi to, co chcesz. Jednak potrzebujemy dodatkowych maszyn w celu zdefiniowania dogodnym 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 

Oto kilka przykładów:

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 

Nie wiem, czy możemy uniknąć definiowania IsPowerOfTwo dla każdej potęgi dwójki.

Aktualizacja: tutaj jest inny wariant bSortN:

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 

Przykład:

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