[Haskell-cafe] Scrap your rolls/unrolls

Max Bolingbroke batterseapower at hotmail.com
Sat Oct 23 12:07:50 EDT 2010

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

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


More information about the Haskell-Cafe mailing list