hello,
ergh, its been a while since i looked at that paper, but basically for
functors with +ve and -ve recursion, the cata(fold) and ana(unfold)
morphisms work together. details can be found in
for example "Domains and lambda calculi" by Amadio and Curien, or Andy
Pitts' "Relational properties of domains". Here is some Haskell code
to illustrate what is going on:
-- What 'G' does to objects.
type G x y = x -> y
-- What 'G' does to arrows.
fun :: (a -> x, y -> b) -> (G x y -> G a b)
fun (j,i) f = i . f . j
-- The "fixpoint"
newtype A = A { unA :: A -> A }
-- The 'cata' and 'ana' are mutually recursive.
univ :: (x -> G y x, G x y -> y) -> (x -> A,A -> y)
univ (j,i) = (ana,cata)
where
cata = i . fun (ana, cata) . unA
ana = A . fun (cata, ana) . j
hope this helps
-Iavor
On Tue, 8 Feb 2005 20:06:25 +0100, Johan Glimming
Hi
I have a problem with contravariance in the bananas in space setting. If you take catamorphism from a function space such as A=A->A to a type such as BxC, then the negative occurrence of X in the functor GXY=X->Y swaps around BxC into B+C.
This means that maybe in this particular case Meijer-Hutton's original Haskell code for cata/ana does not work, since the type for cata would force BxC and B+C to be the same type.
I might be wrong about this, and I wonder anybody can comment on this.
Med vänliga hälsningar / Yours Sincerely, Johan Glimming _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe