创建一个折叠函数，允许在每次重复函数调用后更改类型，以便在不使用递归的情况下调用函数n次。

Question

我正在尝试使用一个定义在这里的dfold

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 

我继续制作了一个更一般化的版本。

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 次。

• 我正在使用 CLaSH 将其综合到 VHDL 中，因此我不能使用递归来应用 t 次

• 我们总是将大小为 2^t 的向量排序为相同大小的向量

• “Vec n a” 是大小为 n 类型为 a 的向量

我想制作一个函数，为给定的 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.

**编辑** 添加了更多细节。

- LambdaScientist

---

让我们在聊天中继续这个讨论。 (http://chat.stackoverflow.com/rooms/135612/discussion-between-lambdascientist-and-user2407038) - LambdaScientist

你到底想填什么（也许是generateBitonicSortN2的主体部分）？我很难看出你提供的哪些函数是硬性约束条件，哪些函数是你提出的解决方案的一部分，以及实际问题是什么。 - Alec

Answer 1

您的基本情况是错误的；它应该是：

您的base情况是错误的；它应该是

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

将所有内容放在一起，这是一个完全可用的版本，在GHC 8.0.2上进行了测试（但它应该在基于GHC 8.0.2的CLaSH上同样有效，除了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>

- Cactus

Answer 2

我正在使用CLaSH将其综合为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

我不知道是否可以避免为每个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)

- effectfully