This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

[Caml-list] First order compile time functorial polymorphism in Ocaml
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: -- (:) From: Michal Moskal Subject: Re: [Caml-list] First order compile time functorial polymorphism in Ocaml
```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

```