[Haskell-cafe] Scrap your rolls/unrolls
Bertram Felgenhauer
bertram.felgenhauer at googlemail.com
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
http://int-e.cohomology.org/~bf3/haskell/Fix.hs
Best regards,
Bertram
More information about the Haskell-Cafe
mailing list