Tạo một lần mà cho phép các loại thay đổi sau mỗi lần gọi hàm lặp đi lặp lại, để gọi một hàm n lần mà không đệ quy

Question

Tôi cố gắng để sử dụng một dfold định nghĩa 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 

Về cơ bản nó là một lần mà cho phép bạn trả lại loại mới sau mỗi chu kỳ.

Tôi cố gắng để khái quát hóa bitonicSort quy định tại dự án này: https://github.com/adamwalker/clash-utils/blob/master/src/CLaSH/Sort.hs

tôi hai chức năng quan trọng cho các loại rằng dfold với generate:

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 

Ví dụ sử dụng trong dự án được đề cập ở trên là:

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 

Tôi đã đi trước d đã tạo ra một phiên bản tổng quát hơn.

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) 

Với phiên bản này, tôi nhanh chóng có thể làm cho Sắp xếp Bitonic mới như vậy:

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 

Mỗi Sắp xếp công việc với một vector có kích thước quy định.

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 

ghi chú nhanh:

• Tôi cố gắng để các áp dụng "genBitonic" thành "bitonicBase" lần t.

• Tôi đang sử dụng Clash để tổng hợp này để VHDL, vì vậy tôi không thể sử dụng đệ quy để áp dụng t lần

• Chúng tôi sẽ luôn luôn được sắp xếp một kích thước vec 2^t vào một vec có cùng kích thước

• "Vec na" là một vector của các kích thước n và gõ một

tôi muốn thực hiện một chức năng mà tạo ra các chức năng cho một Vec nhất định. Tôi tin rằng bằng cách sử dụng dfold hoặc dtfold, là con đường chính xác ở đây.

Tôi muốn làm gấp với chức năng như genBitonic.

Sau đó, sử dụng fst để lấy hàm tôi cần để sắp xếp.

tôi có hai kiểu dáng thể:

Một: Gấp sử dụng thành phần để có được một chức năng rằng có cơ sở.

bSort8 :: Ord a => Vec 8 a -> Vec 8 a 
bSort8 = fst $ genBitonic.genBitonic.genBitonic $ bitonicBase 

Trước khi cơ sở đã được trả lời nó sẽ có kết quả trong một cái gì đó giống như

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

Hai: ý tưởng thứ hai là sử dụng các bitonicBase như giá trị b để bắt đầu tích lũy trên. Điều này sẽ dẫn đến kết quả trực tiếp trong biểu mẫu tôi cần trước khi tôi áp dụng fst.

Chỉnh sửa vecAcum chỉ có nghĩa là giá trị xây dựng bên trong của dfold.

Trong ví dụ dfold họ gấp sử dụng một :> mà chỉ là dạng vector của các nhà điều hành danh sách :

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

Những gì tôi muốn làm là lấy một tuple của hai chức năng như:

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) 

Và soạn chúng. Vì vậy genBitonic . genBitonic sẽ phải loại:

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

Vì vậy, sau đó các chức năng cơ bản sẽ là những gì củng cố các loại. ví dụ:

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 

Tôi đang sử dụng lệnh dfold để tạo hàm cho vectơ có độ dài n tương đương với thực hiện đệ quy trên vectơ có độ dài n.

tôi đã cố gắng:

tôi cố gắng làm theo tấm gương được liệt kê dưới 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 

Tôi đang sử dụng các phần mở rộng mã nguồn dfold sử dụng

{-# 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 #-} 

Lỗi tin nhắn:

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. 

** CHỈNH SỬA ** Đã thêm nhiều chi tiết hơn.

Answer 1

Trường hợp base của bạn không đúng; nó phải được

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

Đưa nó tất cả cùng nhau, đây là một phiên bản làm việc đầy đủ, thử nghiệm trên GHC 8.0.2 (nhưng nó phải làm việc tất cả cùng trên một cuộc đụng độ GHC 8.0.2-based, modulo những thứ Prelude nhập khẩu). Nó chỉ ra điều operationList không được sử dụng ngoại trừ cột sống của nó, vì vậy chúng tôi có thể sử dụng một Vec n() thay thế.

{-# 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) 

Điều này hoạt động như mong đợi, ví dụ::

*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ôi đang sử dụng Clash để tổng hợp này để VHDL, vì vậy tôi không thể sử dụng đệ quy để áp dụng lần t

Tôi không hiểu câu này, nhưng khác hơn là:

{-# 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 được xác định bằng cách đệ quy trên số peano đại diện cho quyền lực. Tại mỗi bước đệ quy, KnownNat (PowerOfTwo p) mới sẽ xuất hiện (thông qua họ loại KnownPowersOfTwo). Ở mức giá trị genBitonicN là không đáng kể và chỉ thực hiện những gì bạn muốn. Tuy nhiên chúng ta cần một số máy móc thiết bị bổ sung để xác định một thuận tiện 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 

Dưới đây là một số ví dụ:

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 

Tôi không biết liệu chúng tôi có thể tránh được xác định IsPowerOfTwo cho mỗi sức mạnh của hai.

Cập nhật: đây là một biến thể của 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 

Một ví dụ:

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