は再帰

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

I二つの機能：私はこのプロジェクトで定義された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 

クイックノート：

• 私は "bitonicBase" のt倍に "genBitonic" を適用しようとしています。

• 私はVHDLにこれを合成するために衝突を使用していますので、私がt回

• を適用するために再帰を使用することはできません我々は常に同じサイズ

のVECにしてVECサイズ2^tでソートされます

• 「はVecとをNa」サイズnのベクトルであり、Iは、所与Vecとする機能を生成する関数を作りたい

を入力します。私はdfoldまたはdtfoldを使うと正しいパスであると信じています。

私は、機能genBitonicのようなもので折り畳みをしたいと思っていました。

次に、fstを使用して、ソートに必要な機能を取得します。

私は2つの可能な設計だった：

ワンを：それはベースをとる関数を得るために組成物を使用して折りたたみます。

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の内側に構築値であることを意味します。

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) 

：彼らは私がやりたいことのように2つの関数のタプルを取るあるリスト演算子 :

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

の単なるベクトル形式である:>を使用して倍dfold例で

それを構成します。 のでgenBitonic . genBitonicはタイプだろう：それでは基本機能は、タイプを固化何だろう

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

を。例：

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を使用しています。

私が試した：

を私は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 #-} 

エラーメッセージを使用して拡張を使用しています：

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. 

** EDIT ** さらに詳しい情報が追加されました。

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) 

これは期待どおりに機能します。：私は、VHDLにこれを合成するために衝突を使用しています

*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

ので、私が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は、パワーを表すpeano番号で再帰によって定義されます。各再帰的ステップで、新しい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 

私たちは2の各電源用のIsPowerOfTwoを定義避けることができるかどうかわかりません。

アップデート：ここ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 

例：

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