[Haskell-cafe] Scrap your rolls/unrolls

[Sjoerd Visscher]

I use Apply for Functor application in data-category, I used an infix operator :%

http://hackage.haskell.org/packages/archive/data-category/0.3.0.1/doc/html/src/Data-Category-Functor.html#line-57

F.e. composition is defined like this:

type instance (g :.: h) :% a = g :% (h :% a)

Sjoerd

On Oct 23, 2010, at 6:07 PM, 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:
> 
> """
> {-# 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
>