How to make catamorphisms work with parameterized/indexed types?

Question

I recently learned a bit about F-algebras: https://www.fpcomplete.com/user/bartosz/understanding-algebras. I wanted to lift this functionality to more advanced types (indexed and higher-kinded). Furthermore, I checked "Giving Haskell a Promotion" (http://research.microsoft.com/en-us/people/dimitris/fc-kind-poly.pdf), which was very helpful because it gave names to my own vague "inventions".

However, I cannot seem to create a unified approach that works for all shapes.

Algebras need some "carrier type", but the structure we're traversing expects a certain shape (itself, applied recursively), so I came up with a "Dummy" container that can carry any type, but is shaped as expected. I then use a type family to couple these.

This approach seems to work, leading to a fairly generic signature for my 'cata' function.

However, the other things I use (Mu, Algebra) still need separate versions for each shape, just for passing a bunch of type variables around. I was hoping something like PolyKinds could help (which I use successfully to shape the dummy type), but it seems it is only meant to work the other way around.

As IFunctor1 and IFunctor2 do not have extra variables, I tried to unify them by attaching (via type family) the index-preserving-function type, but this seems not allowed because of the existential quantification, so I'm left with multiple versions there too.

Is there any way to unify these 2 cases? Did I overlook some tricks, or is this just a limitation for now? Are there other things that can be simplified?

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

And 2 example structures to work with:

ExprF1 seems like a normal useful thing, attaching an embedded type to an object language.

ExprF2 is contrived (extra argument which happens to be lifted (DataKinds) as well), just to find out if the "generic" cata2 is able to handle these shapes.

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

Output:

17
17

Intrastate

It's more uniform to index over pairs than to use two indices. My advice, when working with indexed sets, is to use exactly one index whenever possible, and exploit your freedom to structure the index with promoted types. 1, 2, 4, 8, time to exponentiate! – Unfriendly

@pigworker: ah yes, that's a nice workaround indeed. Then I'll only need cata1 and friends. – Intrastate

Good question, provoking an awesome answer from one of the greats. There can't be many tags where you get to go from basic to sublime. Yay Haskell. – Usage

Answer 1

I wrote a talk on this topic called "Slicing It" in 2009. It certainly points to the work by my Strathclyde colleagues, Johann and Ghani, on initial algebra semantics for GADTs. I used the notation which SHE provides for writing data-indexed types, but that has pleasingly been superseded by the "promotion" story.

The key point of the talk is, as per my comment, to be systematic about using exactly one index, but to exploit the fact that its kind can vary.

So indeed, we have (using my current preferred "Goscinny and Uderzo" names)

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

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

Now you can show FunctorIx is closed under fixpoints. The key is to combine two indexed sets into a one that offers a choice of index.

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)

Now we can now take fixpoints of functors whose "contained elements" stand for either "payload" or "recursive substructures".

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

As a result, we can mapIx over "payload"...

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

...or write a catamorphism over the "recursive substructures"...

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

...or both at once.

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)

The joy of FunctorIx is that it has such splendid closure properties, thanks to the ability to vary the indexing kinds. MuIx allows for notions of payload, and can be iterated. There is thus an incentive to work with structured indices rather than multiple indices.

Unfriendly

Wow. That blew my mind a bit! I can somewhat see how it works, but I can only dream of producing something like that myself. It's very useful in a lot of situations, including my question, so I'm gonna switch the answer to this one. Can you please elaborate a bit what you mean by "closed" and "closure properties" ? I don't have an extensive math-background :( As a sidenote, FunctorIx, FoldIx and friends remind me of a certain caroon :P – Intrastate

The unindexed story defines Mu (f :: * -> *) :: *, where some Functor f describes the node structure of a recursive datatype: f abstracts positions for recursive substructures. But Mu f is not itself a Functor, even if it has a notion of "element". Think about lists: a list node can have a place for a list element and a place for a sublist. You can describe the list Functor by taking the fixpoint of the bifunctor (ie, not the Functor) which describes one node. But recursive indexed functors are fixpoints of other indexed functors. So indexed functors are closed under a fixpoint. – Unfriendly

Answer 2

If I understand it properly, this is precisely the problem tackled by Johann and Ghani's "Initial Algebra Semantics is Enough!"

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

See in particular their hfold

Edit: For the GADT case, see their later paper "Foundations for Structured Programming using GADTs". Note that they encounter an obstacle that can be resolved using PolyKinds, which we now have: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.111.2948

This blog post may also be of interest: http://www.timphilipwilliams.com/posts/2013-01-16-fixing-gadts.html

Topless

Looks like a very interesting paper for sure. However, I'm not sure it deals with my issue though (indexed type through GADT). The last paragraph of the paper explicitly states GADTs are possible future work: "Finally, the techniques of this paper may provide insights into theories of folds, builds, and fusion rules for advanced data types, such as mixed variance data types, GADTs, and dependent types." – Intrastate

Cool, lots to read :) Will probably take me some time to find out if there's a perfect solution in there, but I'm sure it's gonna give me a lot of steps in the right direction, so I'm gonna accept your answer. Thanks! – Intrastate

I had port it to Kmett style recursion schemes gist.github.com/xgrommx/4c72ae9d407214deab55fe9aebc08b45 – Centonze