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>