A little prettier (the cata detour wasn't needed after all): data IdThunk a type instance Force (IdThunk a) = a type Alg f a = f (IdThunk a) -> a fold :: CFunctor f ForceCat (->) => Alg f a -> Fix f -> a fold alg = alg . cmap (ForceCat $ fold alg) sumAlg :: Alg (ListF Int) Int sumAlg Nil = 0 sumAlg (Cons a r) = a + r sumList :: List Int -> Int sumList = fold sumAlg It all works out very well, so this trick seems to be really useful! Sjoerd On Oct 23, 2010, at 4:05 PM, Sjoerd Visscher wrote:

On Oct 23, 2010, at 1:27 PM, Sebastian Fischer wrote:

...

I think `Control.Functor.Categorical.CFunctor` is a more natural replacement for functor here. One can define

instance CFunctor (ListF a) ForceCat Hask

and I was hoping that I could define `fold` based on CFunctor but I did not succeed. The usual definition of `fold` is

fold :: Functor f => (f a -> a) -> Fix f -> a fold f = f . fmap (fold f)

and I tried to replace this with

fold :: CFunctor f ForceCat Hask => ...

but did not find a combination of type signature and definition that compiled.

The catamorphism lies in the ForceCat category. Also, you can't just pass "a" to "f" because Force a is undefined.

data IdThunk a type instance Force (IdThunk a) = a

cata :: CFunctor f ForceCat (->) => (f (IdThunk a) -> a) -> ForceCat (FixThunk f) (IdThunk a) cata alg = ForceCat $ alg . cmap (cata alg)

Then you can define fold as follows:

fold :: CFunctor f ForceCat (->) => (f (IdThunk a) -> a) -> Fix f -> a fold = unForceCat . cata

Fortunately the IdThunk does not get in the way when defining algebras:

sumAlg :: ListF Int (IdThunk Int) -> Int sumAlg Nil = 0 sumAlg (Cons a r) = a + r

greetings, Sjoerd Visscher

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Sjoerd Visscher http://w3future.com

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/s... 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 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

On 2 November 2010 14:10, Bertram Felgenhauer wrote:

Indeed. I had a lot of fun with the ideas of this thread, extending the 'Force' type family (which I call 'Eval' below) to a small EDSL on the type level:

I also came up with this.. I was trying to use it to get two type classes for (Monoid Int) like this, but it doesn't work: """ {-# LANGUAGE TypeFamilies, EmptyDataDecls, ScopedTypeVariables, TypeOperators, FlexibleInstances, FlexibleContexts #-} import Data.Monoid -- Type family for evaluators on types type family E a :: * -- Tag for functor application: fundamental to our approach infixr 9 :% data f :% a -- Tags for evalutor-style data declarations: such declarations contain "internal" -- occurrences of E, so we can delay evaluation of their arguments data P0T (f :: *) type instance E (P0T f) = f data P1T (f :: * -> *) type instance E (P1T f :% a) = f a data P2T (f :: * -> * -> *) type instance E (P2T f :% a :% b) = f a b data P3T (f :: * -> * -> * -> *) type instance E (P3T f :% a :% b :% c) = f a b c -- When applying legacy data types we have to manually force the arguments: data FunT type instance E (FunT :% a :% b) = E a -> E b data Tup2T type instance E (Tup2T :% a :% b) = (E a, E b) data Tup3T type instance E (Tup3T :% a :% b :% c) = (E a, E b, E c) -- Evalutor-style versions of some type classes class FunctorT f where fmapT :: (E a -> E b) -> E (f :% a) -> E (f :% b) class MonoidT a where memptyT :: E a mappendT :: E a -> E a -> E a data AdditiveIntT type instance E AdditiveIntT = Int instance MonoidT AdditiveIntT where memptyT = 0 mappendT = (+) data MultiplicativeIntT type instance E MultiplicativeIntT = Int instance MonoidT MultiplicativeIntT where memptyT = 1 mappendT = (*) -- Make the default instance of Monoid be additive: instance MonoidT (P0T Int) where memptyT = memptyT :: E AdditiveIntT mappendT = mappendT :: E AdditiveIntT -> E AdditiveIntT -> E AdditiveIntT main = do print (result :: E (P0T Int)) print (result :: E MultiplicativeIntT) where result :: forall a. (E a ~ Int, MonoidT a) => E a result = memptyT `mappendT` 2 `mappendT` 3 """ The reason it doesn't work is clear: it is impossible to tell GHC which MonoidT Int dictionary you intend to use, since E is not injective! I think this is a fundamental flaw in the scheme.

The implementation is somewhat verbose, but quite straight-forward tree manipulation.

This is impressively mad. You can eliminate phase 1 by introducing the identity code (at least, it typechecks): """ data Id type instance Eval (App Id a) = Eval a """ """ type instance Eval (Fix a) = Eval (Fix1 a Id) data Fix1 a b -- compositions, phase 2.: build left-associative composition type instance Eval (Fix1 (a :.: (b :.: c)) d) = Eval (Fix1 ((a :.: b) :.: c) d) type instance Eval (Fix1 (a :.: Id) c) = Eval (Fix1 a c) type instance Eval (Fix1 (a :.: ConE b) c) = Eval (Fix1 a (ConE b :.: c)) type instance Eval (Fix1 (a :.: Con1 b) c) = Eval (Fix1 a (Con1 b :.: c)) -- compositions, final step: apply first element to fixpoint of shifted cycle type instance Eval (Fix1 Id b) = Eval (Fix b) type instance Eval (Fix1 (ConE a) b) = a (Fix (b :.: ConE a)) type instance Eval (Fix1 (Con1 a) b) = a (Eval (Fix (b :.: Con1 a))) """ I'm not sure whether this formulation is clearer or not. Cheers, Max