创建折叠，允许类型到每个重复函数调用之后改变，以调用一个函数的n倍，而不递归

我试图使用dfold定义here 创建折叠，允许类型到每个重复函数调用之后改变，以调用一个函数的n倍，而不递归

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在这个项目定义： https://github.com/adamwalker/clash-utils/blob/master/src/CLaSH/Sort.hs

我两个功能是为与dfold产生的各类重要：

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

的例子中使用上述项目是：

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制作了更通用的版本。

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)

有了这个版本，我可以快速作出新的双调排序，像这样：

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

每个排序与指定大小的矢量工作。

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次
我们将始终在被分拣A VEC大小2^T同样大小的A VEC
“VEC NA”是大小为n的向量，并输入一个

我想使产生用于给定的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)

两个：设想二是使用bitonicBase作为b的值就开始积累。这会直接导致我在申请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)

并撰写它们。所以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

我使用dfold搭建长度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 #-}

错误消息：

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.

**编辑** 增加了更多的细节。

来源

2017-02-12 LambdaScientist

让我们[继续聊天讨论]（http://chat.stackoverflow.com/rooms/135612 /讨论-之间-lambdascientist和 - user2407038）。 – LambdaScientist

你究竟想要填什么（可能是'generateBitonicSortN2'的主体）？我很难看到你给出的功能是硬约束，哪些功能是你提出的解决方案的一部分，以及实际的问题是什么。 – Alec

您的base案件有误;它应该是

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

全部放在一起，这里有一个充分的工作版本，在GHC 8.0.2测试（但它应该工作在基于8.0.2-GHC冲突都是一样的，取模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>

来源

2017-03-07 08:17:29 Cactus

我使用的冲突，以合成该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通过递归表示功率的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

我不知道我们是否能够避免定义为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)

来源

2017-03-08 15:27:55 user3237465

创建折叠，允许类型到每个重复函数调用之后改变，以调用一个函数的n倍，而不递归

回答

相关问题