On 23 October 2010 15:32, Sjoerd Visscher
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