文档建议反馈控制台
首页
学习
活动
专区
工具
TVP
最新优惠活动
文章/答案/技术大牛
发布
社区首页 >问答首页 >创建一个允许在每次重复的函数调用后更改类型的文件夹，以便在没有递归的情况下调用函数n次

问创建一个允许在每次重复的函数调用后更改类型的文件夹，以便在没有递归的情况下调用函数n次
EN

Stack Overflow用户
提问于 2017-02-13 01:58:28
回答 2查看 584关注 0票数 19

我正在尝试使用dfold定义的here

代码语言：javascript
复制
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生成的类型很重要：

代码语言：javascript
复制
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

上面提到的项目中使用的示例如下：

代码语言：javascript
复制
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

我继续做了一个更通用的版本。

代码语言：javascript
复制
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)

使用这个版本，我可以快速创建新的Bitonic排序，如下所示：

代码语言：javascript
复制
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

每个排序都使用指定大小的向量。

代码语言：javascript
复制
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获取排序所需的函数。

我有两种可能的设计：

One：使用组合进行折叠，得到一个带基的函数。

代码语言：javascript
复制
bSort8 :: Ord a => Vec 8 a -> Vec 8 a
bSort8 = fst $ genBitonic.genBitonic.genBitonic $ bitonicBase

在基础回复之前，它可能会导致类似这样的结果

代码语言：javascript
复制
**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)

Two：第二个想法是使用bitonicBase作为开始累加的值b。这将直接导致在应用fst之前我需要它的表单。

编辑 vecAcum只是为了在dfold中建立价值。

在dfold示例中，它们使用列表运算符:的向量形式的:>进行折叠

代码语言：javascript
复制
>>> :t (:>)
(:>) :: a -> Vec n a -> Vec (n + 1) a

我想要做的是获取两个函数的元组，如下所示：

代码语言：javascript
复制
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的类型为：

代码语言：javascript
复制
(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)

因此，基函数将是巩固类型的基础。例如：

代码语言：javascript
复制
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下面列出的示例。

代码语言：javascript
复制
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源代码使用的扩展。

代码语言：javascript
复制
{-# 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 #-}

错误消息：

代码语言：javascript
复制
   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.

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

haskell
type-systems
type-level-computation
clash
EN

回答 2

Stack Overflow用户

回答已采纳

发布于 2017-03-07 16:17:30

您的base案例是错误的；它应该是错误的

代码语言：javascript
复制
base :: (Ord a) => SplitHalf a @@ 0
base = (id, bitonicMerge id)

综上所述，这是一个完整的工作版本，在GHC8.0.2上进行了测试(但它应该同样可以在基于GHC8.0.2的CLaSH上工作，对Prelude导入内容进行模块化)。事实证明，除了脊椎之外，不使用operationList对象，因此我们可以使用Vec n ()。

代码语言：javascript
复制
{-# 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)

这就像预期的那样工作，例如：

代码语言：javascript
复制
*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>
票数 5
EN

Stack Overflow用户

发布于 2017-03-08 23:27:55

我用CLaSH把它综合成

，所以我不能用递归来应用t次

我不明白这句话，但除此之外：

代码语言：javascript
复制
{-# 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

代码语言：javascript
复制
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

下面是一些示例：

代码语言：javascript
复制
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的另一个变体

代码语言：javascript
复制
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

举个例子：

代码语言：javascript
复制
bSort16 :: Ord a => OnVec 16 a
bSort16 = bSortNP (Proxy :: Proxy 4)
票数 1
EN
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：

https://stackoverflow.com/questions/42191163

复制
相关文章

相似问题

领券

腾讯云开发者

扫码关注腾讯云开发者

扫码关注腾讯云开发者

领取腾讯云代金券

热门产品

热门推荐

更多推荐

Copyright © 2013 - 2024 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有 

深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 深公网安备号 44030502008569

腾讯云计算（北京）有限责任公司 京ICP证150476号 |  京ICP备11018762号 | 京公网安备号11010802020287

问题归档专栏文章快讯文章归档关键词归档开发者手册归档开发者手册 Section 归档