Iavor Diatchki iavor.diatchki at gmail.com
Wed Feb 9 13:28:26 EST 2005

```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 <glimming at kth.se> wrote:
> 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.
>