Version française
Home     About     Download     Resources     Contact us    

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

Browse thread
[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: 2003-06-23 (10:27)
From: Markus Mottl <markus@o...>
Subject: Re: [Caml-list] First order compile time functorial polymorphism in Ocaml
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 ;-)

Markus Mottl

Markus Mottl

To unsubscribe, mail Archives:
Bug reports: FAQ:
Beginner's list: