[Haskell-cafe] Contravariance

[Iavor Diatchki]

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.
> 
> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>