Re: [Caml-list] First order compile time functorial polymorphism in Ocaml

[Markus Mottl <markus@oefai.at>]

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

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

Sorry for my nitpicking ;-)

Regards,
Markus Mottl

-- 
Markus Mottl          http://www.oefai.at/~markus          markus@oefai.at

-------------------
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