[Haskell-cafe] Scrap your rolls/unrolls

[Max Bolingbroke]

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:

"""
{-# LANGUAGE TypeFamilies, EmptyDataDecls #-}

type family Foo a :: *
type instance Foo Int = Bool
type instance Foo Bool = Int

type family Bar a :: *
type instance Bar Int = Char
type instance Bar Bool = Char
"""

Now you want to build a data type where you have abstracted over the
particular type family to apply:

"""
data GenericContainer f_clo = GC (f_clo Int) (f_clo Bool)
type FooContainer = GenericContainer Foo
type BarContainer = GenericContainer Bar
"""

This is a very natural thing to do, but it is rejected by GHC because
Foo and Bar are partially applied in FooContainer and BarContainer.
You can work around this by "eta expanding" Foo/Bar using a newtype,
but it is more elegant to scrap your newtype injections/extractions
with the trick:

"""
data FooClosure
data BarClosure


type family Apply f a :: *
type instance Apply FooClosure a = Foo a
type instance Apply BarClosure a = Bar a


data GenericContainer f_clo = GC (Apply f_clo Int) (Apply f_clo Bool)
type FooContainer = GenericContainer FooClosure
type BarContainer = GenericContainer BarClosure
"""

These definitions typecheck perfectly:

"""
valid1 :: FooContainer
valid1 = GC True 1

valid2 :: BarContainer
valid2 = GC 'a' 'b'
"""

With type functions, Haskell finally type-level lambda of a sort :-)

Cheers,
Max