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 <sjo...@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 > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe