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

标签 haskell type-systems type-level-computation clash

我正在尝试使用定义的 dfold 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

基本上它是一个折叠，允许您在每个循环后返回一个新类型。

我试图概括 双音排序 在这个项目中定义:
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 排序为相同大小的 vec
  • "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 内部建立值(value)。 .

    在 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.

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

    最佳答案

    您的 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>

    关于haskell - 创建一个折叠，允许在每次重复的函数调用后更改类型，以便在不递归的情况下调用函数 n 次，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/42191163/

    上一篇：common-lisp - Clozure CL 编译的可执行文件丢失某些命令行参数

    下一篇：emacs - 遍历到 Lispworks 中的匹配括号

    相关文章：

    list - 尝试获取最后一个元素时出现 Haskell 错误

    c# - 如果将结构类型添加到 C# 中，需要更改什么？

    language-agnostic - 我对类型系统的理解正确吗？

    haskell - 术语级时钟频率访问

    scala - 具有继承类型的 Aux 模式推理失败

    list - 创建保存另一种数据类型的特定值的数据类型

    haskell - 跳过 monad 中剩余的操作 - 类似 return

    c# - 如何在 C# 中使用类的类型作为继承的集合属性的类型参数

    typescript - 翻转文字记录类型中的键和值

    haskell - 为什么某些 Data.List.Split 函数使用 `Int` 而其他函数使用 `Integral a` ？

    ©2024 IT工具网  联系我们