haskell - resueltos - Creación de un pliegue que permite que el tipo cambie después de cada llamada de función repetida, para llamar a una función n veces sin recursión

recursividad ejemplos resueltos

Question

Estoy tratando de usar un dfold definido 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

Básicamente es un pliegue que te permite devolver un nuevo tipo después de cada ciclo.

Estoy tratando de generalizar el bitonicSort definido en este proyecto: https://github.com/adamwalker/clash-utils/blob/master/src/CLaSH/Sort.hs

Tengo dos funciones que son importantes para los tipos que dfold genera:

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

El ejemplo utilizado en el proyecto mencionado anteriormente es:

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 

Seguí adelante e hice una versión más general.

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)

Con esta versión puedo hacer rápidamente nuevos tipos de Bitonic así:

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

Cada Ordenar con trabajo con un vector del tamaño especificado.

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

Notas rápidas:

• Estoy tratando de aplicar "genBitonic" a "bitonicBase" t veces.

• Estoy usando CLaSH para sintetizar esto en VHDL, por lo que no puedo usar la recursión para aplicar t veces

• Siempre estaremos clasificando un tamaño vec 2 ^ t en un vec del mismo tamaño

• "Vec na" es un vector de tamaño n y tipo a

Me gustaría hacer una función que genere la función para un Vec dado. Creo que usar dfold o dtfold, es el camino correcto aquí.

Quería hacer el pliegue con algo como la función genBitonic .

Luego usa fst para obtener la función que necesito para clasificar.

Tuve dos posibles diseños:

Uno : Dobla usando la composición para obtener una función que tome una base.

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

Antes de que la base fuera contestada, habría resultado en algo como

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

Dos : la segunda idea fue usar bitonicBase como el valor b para comenzar a acumular. Esto hubiera resultado directamente en el formulario en el que lo necesito antes de aplicar fst .

Editar vecAcum solo debe ser el valor que se acumula dentro del dfold .

En el ejemplo dfold, se pliegan usando un :> que es solo la forma vectorial del operador de lista :

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

Lo que quiero hacer es tomar una tupla de dos funciones como:

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)

Y componerlos. Tan genBitonic . genBitonic genBitonic . genBitonic tendría tipo:

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

Entonces, la función base sería lo que solidifica los tipos. p.ej

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

Estoy usando dfold para construir la función para Vectores de longitud n que es equivalente a hacer la recursión en un vector de longitud n.

Lo intenté:

Traté de seguir el ejemplo que figura en 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

Estoy usando las extensiones que usa el código fuente 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 #-}

Error de mensajes:

 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.

** EDIT ** Añadido mucho más detalle.

Answer 1

Estoy usando CLaSH para sintetizar esto en VHDL, por lo que no puedo usar la recursión para aplicar t veces

No entiendo esta frase, pero aparte de eso:

{-# 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 se define por la recursión en el número peano que representa una potencia. En cada paso recursivo aparece un nuevo KnownNat (PowerOfTwo p) (a través de la familia de tipos KnownPowersOfTwo ). En el nivel de valor, genBitonicN es trivial y solo hace lo que usted quiere. Sin embargo, necesitamos un poco de maquinaria adicional para definir un bSortN conveniente:

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

Aquí hay unos ejemplos:

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

No sé si podemos evitar definir IsPowerOfTwo para cada potencia de dos.

Actualización: aquí hay otra variante de 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

Un ejemplo:

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

Answer 2

Su caso base estaba equivocado; debería ser

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

Poniéndolo todo junto, aquí hay una versión completamente funcional, probada en GHC 8.0.2 (pero debería funcionar de la misma manera en un CLaSH basado en GHC 8.0.2, en módulo la materia de importación de Prelude ). Resulta que la operationList no se usa a excepción de su espina dorsal, así que podemos usar un Vec n () lugar.

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

Esto funciona como se espera, por ejemplo:

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