[Haskell-cafe] Scrap your rolls/unrolls

[Bertram Felgenhauer]

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

  http://int-e.cohomology.org/~bf3/haskell/Fix.hs

Best regards,

Bertram