Come far funzionare i catamorfismi con tipi parametrici/indicizzati?

Question

Recentemente ho appreso un po 'di F-algebre: https://www.fpcomplete.com/user/bartosz/understanding-algebras. Volevo trasferire questa funzionalità a tipi più avanzati (indicizzati e di livello superiore). Inoltre, ho controllato "Giving Haskell a Promotion" (http://research.microsoft.com/en-us/people/dimitris/fc-kind-poly.pdf), che è stato molto utile perché ha dato nomi alle mie "invenzioni" vaghe.

Tuttavia, non riesco a creare un approccio unificato che funzioni per tutte le forme.

Algebras bisogno di qualche "tipo vettore", ma la struttura che stiamo attraversando si aspetta una certa forma (per sé, applicato ricorsivamente), così sono venuto con un contenitore "Dummy" che può trasportare qualsiasi tipo, ma è conformato previsto. Quindi uso una famiglia di tipi per accoppiarli.

Questo approccio sembra funzionare, portando a una firma abbastanza generica per la mia funzione 'cata'.

Tuttavia, le altre cose che uso (Mu, Algebra) hanno ancora bisogno di versioni separate per ogni forma, solo per il passaggio di un gruppo di variabili di tipo. Speravo che qualcosa come PolyKinds potesse essere d'aiuto (che uso con successo per modellare il tipo fittizio), ma sembra che abbia solo lo scopo di funzionare al contrario.

Poiché IFunctor1 e IFunctor2 non hanno variabili aggiuntive, ho provato a unificarle allegando (tramite famiglia di tipi) il tipo di funzione di conservazione dell'indice, ma ciò non è consentito a causa della quantificazione esistenziale, quindi sono rimasto con più versioni anche lì.

C'è un modo per unificare questi 2 casi? Ho trascurato alcuni trucchi, o è solo una limitazione per ora? Ci sono altre cose che possono essere semplificate?

{-# LANGUAGE DataKinds     #-} 
{-# LANGUAGE ExistentialQuantification #-} 
{-# LANGUAGE GADTs      #-} 
{-# LANGUAGE PolyKinds     #-} 
{-# LANGUAGE Rank2Types    #-} 
{-# LANGUAGE StandaloneDeriving  #-} 
{-# LANGUAGE TypeFamilies    #-} 
{-# LANGUAGE TypeOperators    #-} 
{-# LANGUAGE UndecidableInstances  #-} 
module Cata where 

-- 'Fix' for indexed types (1 index) 
newtype Mu1 f a = Roll1 { unRoll1 :: f (Mu1 f) a } 
deriving instance Show (f (Mu1 f) a) => Show (Mu1 f a) 

-- 'Fix' for indexed types (2 index) 
newtype Mu2 f a b = Roll2 { unRoll2 :: f (Mu2 f) a b } 
deriving instance Show (f (Mu2 f) a b) => Show (Mu2 f a b) 

-- index-preserving function (1 index) 
type s :-> t = forall i. s i -> t i 

-- index-preserving function (2 index) 
type s :--> t = forall i j. s i j -> t i j 

-- indexed functor (1 index) 
class IFunctor1 f where 
    imap1 :: (s :-> t) -> (f s :-> f t) 

-- indexed functor (2 index) 
class IFunctor2 f where 
    imap2 :: (s :--> t) -> (f s :--> f t) 

-- dummy container type to store a solid result type 
-- the shape should follow an indexed type 
type family Dummy (x :: i -> k) :: * -> k 

type Algebra1 f a = forall t. f ((Dummy f) a) t -> (Dummy f) a t 
type Algebra2 f a = forall s t. f ((Dummy f) a) s t -> (Dummy f) a s t 

cata1 :: IFunctor1 f => Algebra1 f a -> Mu1 f t -> (Dummy f) a t 
cata1 alg = alg . imap1 (cata1 alg) . unRoll1 

cata2 :: IFunctor2 f => Algebra2 f a -> Mu2 f s t -> (Dummy f) a s t 
cata2 alg = alg . imap2 (cata2 alg) . unRoll2 

E 2 strutture di esempio per lavorare con:

ExprF1 sembra una cosa utile normale, allegando un tipo incorporato per un linguaggio object.

ExprF2 è escogitato (argomento extra che capita di essere sollevato (DataKinds)), solo per scoprire se il cata2 "generico" è in grado di gestire queste forme.

-- our indexed type, which we want to use in an F-algebra (1 index) 
data ExprF1 f t where 
    ConstI1 :: Int -> ExprF1 f Int 
    ConstB1 :: Bool -> ExprF1 f Bool 
    Add1 :: f Int -> f Int -> ExprF1 f Int 
    Mul1 :: f Int -> f Int -> ExprF1 f Int 
    If1  :: f Bool -> f t -> f t -> ExprF1 f t 
deriving instance (Show (f t), Show (f Bool)) => Show (ExprF1 f t) 

-- our indexed type, which we want to use in an F-algebra (2 index) 
data ExprF2 f s t where 
    ConstI2 :: Int -> ExprF2 f Int True 
    ConstB2 :: Bool -> ExprF2 f Bool True 
    Add2 :: f Int True -> f Int True -> ExprF2 f Int True 
    Mul2 :: f Int True -> f Int True -> ExprF2 f Int True 
    If2  :: f Bool True -> f t True -> f t True -> ExprF2 f t True 
deriving instance (Show (f s t), Show (f Bool t)) => Show (ExprF2 f s t) 

-- mapper for f-algebra (1 index) 
instance IFunctor1 ExprF1 where 
    imap1 _ (ConstI1 x) = ConstI1 x 
    imap1 _ (ConstB1 x) = ConstB1 x 
    imap1 eval (x `Add1` y) = eval x `Add1` eval y 
    imap1 eval (x `Mul1` y) = eval x `Mul1` eval y 
    imap1 eval (If1 p t e) = If1 (eval p) (eval t) (eval e) 

-- mapper for f-algebra (2 index) 
instance IFunctor2 ExprF2 where 
    imap2 _ (ConstI2 x) = ConstI2 x 
    imap2 _ (ConstB2 x) = ConstB2 x 
    imap2 eval (x `Add2` y) = eval x `Add2` eval y 
    imap2 eval (x `Mul2` y) = eval x `Mul2` eval y 
    imap2 eval (If2 p t e) = If2 (eval p) (eval t) (eval e) 

-- turned into a nested expression 
type Expr1 = Mu1 ExprF1 

-- turned into a nested expression 
type Expr2 = Mu2 ExprF2 

-- dummy containers 
newtype X1 x y = X1 x deriving Show 
newtype X2 x y z = X2 x deriving Show 

type instance Dummy ExprF1 = X1 
type instance Dummy ExprF2 = X2 


-- a simple example agebra that evaluates the expression 
-- turning bools into 0/1  
alg1 :: Algebra1 ExprF1 Int 
alg1 (ConstI1 x)   = X1 x 
alg1 (ConstB1 False)  = X1 0 
alg1 (ConstB1 True)   = X1 1 
alg1 ((X1 x) `Add1` (X1 y)) = X1 $ x + y 
alg1 ((X1 x) `Mul1` (X1 y)) = X1 $ x * y 
alg1 (If1 (X1 0) _ (X1 e)) = X1 e 
alg1 (If1 _ (X1 t) _)  = X1 t 

alg2 :: Algebra2 ExprF2 Int 
alg2 (ConstI2 x)   = X2 x 
alg2 (ConstB2 False)  = X2 0 
alg2 (ConstB2 True)   = X2 1 
alg2 ((X2 x) `Add2` (X2 y)) = X2 $ x + y 
alg2 ((X2 x) `Mul2` (X2 y)) = X2 $ x * y 
alg2 (If2 (X2 0) _ (X2 e)) = X2 e 
alg2 (If2 _ (X2 t) _)  = X2 t 


-- simple helpers for construction 
ci1 :: Int -> Expr1 Int 
ci1 = Roll1 . ConstI1 

cb1 :: Bool -> Expr1 Bool 
cb1 = Roll1 . ConstB1 

if1 :: Expr1 Bool -> Expr1 a -> Expr1 a -> Expr1 a 
if1 p t e = Roll1 $ If1 p t e 

add1 :: Expr1 Int -> Expr1 Int -> Expr1 Int 
add1 x y = Roll1 $ Add1 x y 

mul1 :: Expr1 Int -> Expr1 Int -> Expr1 Int 
mul1 x y = Roll1 $ Mul1 x y 

ci2 :: Int -> Expr2 Int True 
ci2 = Roll2 . ConstI2 

cb2 :: Bool -> Expr2 Bool True 
cb2 = Roll2 . ConstB2 

if2 :: Expr2 Bool True -> Expr2 a True-> Expr2 a True -> Expr2 a True 
if2 p t e = Roll2 $ If2 p t e 

add2 :: Expr2 Int True -> Expr2 Int True -> Expr2 Int True 
add2 x y = Roll2 $ Add2 x y 

mul2 :: Expr2 Int True -> Expr2 Int True -> Expr2 Int True 
mul2 x y = Roll2 $ Mul2 x y 


-- test case 
test1 :: Expr1 Int 
test1 = if1 (cb1 True) 
      (ci1 3 `mul1` ci1 4 `add1` ci1 5) 
      (ci1 2) 

test2 :: Expr2 Int True 
test2 = if2 (cb2 True) 
      (ci2 3 `mul2` ci2 4 `add2` ci2 5) 
      (ci2 2) 


main :: IO() 
main = let (X1 x1) = cata1 alg1 test1 
      (X2 x2) = cata2 alg2 test2 
     in do print x1 
      print x2 

uscita:

17 
17 

Answer 1

ho scritto un discorso su questo argomento chiamato "Slicing It" nel 2009. E ' Indica certamente il lavoro dei miei colleghi di Strathclyde, Johann e Ghani, sulla semantica di algebra iniziale per GADT.Ho usato la notazione che SHE fornisce per la scrittura di tipi indicizzati dai dati, ma che è stata piacevolmente sostituita dalla storia della "promozione".

Il punto chiave del discorso è, come per il mio commento, essere sistematico sull'utilizzo di un solo indice, ma per sfruttare il fatto che il suo tipo può variare.

Così in effetti, abbiamo (usando le mie attuali nomi preferiti "Goscinny e Uderzo")

type s :-> t = forall i. s i -> t i 

class FunctorIx f where 
    mapIx :: (s :-> t) -> (f s :-> f t) 

Ora è possibile mostrare FunctorIx è chiuso sotto punti di rilevamento. La chiave è combinare due insiemi indicizzati in uno che offre una scelta di indice.

data Case (f :: i -> *) (g :: j -> *) (b :: Either i j) :: * where 
    L :: f i -> Case f g (Left i) 
    R :: g j -> Case f g (Right j) 

(<?>) :: (f :-> f') -> (g :-> g') -> Case f g :-> Case f' g' 
(f <?> g) (L x) = L (f x) 
(f <?> g) (R x) = R (g x) 

Ora possiamo ora prendere punti fissi di funtori cui "elementi contenuti" stand sia per "payload" o "sottostrutture ricorsive".

data MuIx (f :: (Either i j -> *) -> j -> *) :: (i -> *) -> j -> * where 
    InIx :: f (Case x (MuIx f x)) j -> MuIx f x j 

Di conseguenza, siamo in grado di mapIx over "payload" ...

instance FunctorIx f => FunctorIx (MuIx f) where 
    mapIx f (InIx xs) = InIx (mapIx (f <?> mapIx f) xs) 

... o scrivere un catamorphism sopra ai "sottostrutture ricorsive" ...

foldIx :: FunctorIx f => (f (Case x t) :-> t) -> MuIx f x :-> t 
foldIx f (InIx xs) = f (mapIx (id <?> foldIx f) xs) 

... o entrambi contemporaneamente.

mapFoldIx :: FunctorIx f => (x :-> y) -> (f (Case y t) :-> t) -> MuIx f x :-> t 
mapFoldIx e f (InIx xs) = f (mapIx (e <?> mapFoldIx e f) xs) 

La gioia FunctorIx è che ha così splendidi proprietà di chiusura, grazie alla possibilità di variare il tipo di indicizzazione. MuIx consente le nozioni di payload e può essere iterato. C'è quindi un incentivo a lavorare con indici strutturati piuttosto che con più indici.

Answer 2

Se ho capito correttamente, è proprio questo il problema affrontato da Johann e Ghani di "Algebra Semantica iniziale è abbastanza!"

https://personal.cis.strath.ac.uk/neil.ghani/papers/ghani-tlca07.pdf

Si veda in particolare la loro hfold

Edit: Per il caso GADT, vedere la loro carta più avanti "Fondamenti di programmazione strutturata utilizzando GADTs". Si noti che incontrano un ostacolo che può essere risolto utilizzando PolyKinds, che abbiamo ora: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.111.2948

Questo post del blog può anche essere di interesse: http://www.timphilipwilliams.com/posts/2013-01-16-fixing-gadts.html