Tue Nov 2 10:10:48 EDT 2010

```Max Bolingbroke wrote:
> On 23 October 2010 15:32, Sjoerd Visscher <sjoerd at w3future.com> wrote:
> > A little prettier (the cata detour wasn't needed after all):
> >
> >   data IdThunk a
> >   type instance Force (IdThunk a) = a
>
> Yes, this IdThunk is key - in my own implementation I called this "Forced", so:
>
> """
> type instance Force (Forced a) = a
> """
>
> You can generalise this trick to abstract over type functions, though
> I haven't had a need to do this yet. Let us suppose you had these
> definitions:
...
> With type functions, Haskell finally type-level lambda of a sort :-)

Indeed. I had a lot of fun with the ideas of this thread, extending
the 'Force' type family (which I call 'Eval' below) to a small EDSL
on the type level:

The EDSL supports constants

data Con (t :: *)        -- type constant
data Con1 (t :: * -> *)  -- unary type constructor
data ConE (t :: * -> *)  -- like Con1, but the argument is used with Eval

and a few operators

data App a b             -- apply a to b
data Fix a               -- compute fixpoint of a
data a :.: b             -- compose two unary type constructors

There is a type family Eval that maps expressions from that EDSL to
actual types,

type family Eval t :: *

The basic operations are straight-forward to implement,

type instance Eval (Con t) = t
type instance Eval (App (Con1 t) a) = t (Eval a)
type instance Eval (App (ConE t) a) = t a
type instance Eval (App (a :.: b) c) = Eval (App a (App b c))

Now we turn to fixed points. An easy definition would be

type instance Eval (Fix f) = Eval (App f (Fix f))

Let's play with that. For that, we defined

data TreeF a t = Node a [Eval t]
type Tree a = Eval (Fix (ConE (TreeF a)))

-- works fine in ghc 7.1
-- ghc 6.12.3 chokes on it for the recursive types
deriving instance (Show a, Show (Eval t)) => Show (TreeF a t)

And indeed,

ghci> Node 1 [Node 2 []] :: Tree Int
Node 1 [Node 2 []]

and a lot of other things work as expected. But what if we want to
work with fixed points of the composition of several functors?

This works fine:

type Tree2 a b = Eval (Fix (ConE (TreeF a) :.: ConE (TreeF b)))

t0 :: Tree2 Bool Int
t0 = Node True [Node 1 [Node False []]]

t1 :: Tree2 Int Bool
t1 = Node 1 [Node True [Node 1 [Node False []]]]

but this doesn't:

t1 :: Tree2 Int Bool
t1 = Node 1 [t0]

We can help the type checker out by evaluating fixed points for
compositions differently: Instead of applying the whole sequence
of functors at once, apply them one by one, and keep the remaining
sequence in a nice shape so that the type checker can identify
equivalent compositions.

The implementation is somewhat verbose, but quite straight-forward
tree manipulation.

-- easy case first
type instance Eval (Fix (ConE f)) = f (Fix (ConE f))

-- handle compositions, phase 1.: find last element.
type instance Eval (Fix (a :.: (b :.: c))) = Eval (Fix ((a :.: b) :.: c))
type instance Eval (Fix (a :.: (ConE b))) = Eval (Fix1 a (ConE b))
type instance Eval (Fix (a :.: (Con1 b))) = Eval (Fix1 a (Con1 b))

data Fix1 a b
-- compositions, phase 2.: build left-associative composition chain
type instance Eval (Fix1 (a :.: (b :.: c)) d) = Eval (Fix1 ((a :.: b) :.: c) d)
type instance Eval (Fix1 (a :.: ConE b) c) = Eval (Fix1 a (ConE b :.: c))
type instance Eval (Fix1 (a :.: Con1 b) c) = Eval (Fix1 a (Con1 b :.: c))

-- compositions, final step: apply first element to fixpoint of shifted cycle
type instance Eval (Fix1 (ConE a) b) = a (Fix (b :.: ConE a))
type instance Eval (Fix1 (Con1 a) b) = a (Eval (Fix (b :.: Con1 a)))

And with that implementation, the above definition of  t1  typechecks.

Full code with more examples is available at