On Mon, Jun 23, 2003 at 12:27:23PM +0200, Markus Mottl wrote:
> On Mon, 23 Jun 2003, Michal Moskal wrote:
> > Variable occurs positively in type, if it's preceded by even number of
> > negations.
> > 
> > When you treat -> as logical implication, you get:
> > 
> >   a -> b == a & !b
> 
> This is incorrect, your right hand side would correspond to !(a -> b).
> The correct, minimal definition of implication in terms of negations,
> conjunctions and disjunctions is:
> 
>   a -> b = !a \/ b

Sorry, you're of course right.

> 
> > So 'a -> t, 'a -> (t -> 'a) are 'a-positive, t -> 'a is 'a-negative,
> > and 'a -> 'a isn't neither 'a positive nor 'a negative. Other tycons
> > (like *) doesn't change sign. But when you define new type, say:
> > 
> >   type ('a, 'b) t = Foo of 'a -> 'b
> > 
> > then ('c, 'd) t is 'd negative, and 'c positive.
> 
> As a consequence, you need to interchange "positive" and "negative"
> against each other in the upper paragraph. Then "covariant" and "positive"
> fall together as do "contravariant" and "negative". This is also the
> way OCaml treats variance annotations.

Yes. I just googled for covariant/contravariant and found the same.

-- 
: Michal Moskal :: http://www.kernel.pl/~malekith : GCS {C,UL}++++$ a? !tv
: When in doubt, use brute force. -- Ken Thompson : {E-,w}-- {b++,e}>+++ h

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners