[Caml-list] Difference between [ `A ] and [< `A ]

[Caml-list] Difference between [ `A ] and [< `A ]

[Dario Teixeira]

Hi,

I've seen OCaml code "in the wild" where both of the following signatures
are present: (the type parameter for 't' is a phantom type)

  val foo: [< `A ] t -> unit
  val bar: [ `A ] t -> unit

But is there any practical difference between [ `A ] and [< `A ] given
that there is only one element in the set?

Thanks in advance!
Kind regards,
Dario Teixeira

Re: [Caml-list] Difference between [ `A ] and [< `A ]

[Jacques Garrigue]

On 2011/05/11, at 1:46, Dario Teixeira wrote:

> Hi,
> 
> I've seen OCaml code "in the wild" where both of the following signatures
> are present: (the type parameter for 't' is a phantom type)
> 
>  val foo: [< `A ] t -> unit
>  val bar: [ `A ] t -> unit
> 
> But is there any practical difference between [ `A ] and [< `A ] given
> that there is only one element in the set?

In this particular case the two types are almost equivalent.
The only counterexample I could find is unifying with the following
private row type:

  type leA = private [< `A]

leA is unifiable with [< `A] but not with [`A].

The difference becomes more significant when there is an argument.
For instance, [<  `A of int] and [< `A of bool] are unifiable, giving [< `A of int & bool],
but [`A of int] cannot be unified with [`A of bool].

Note that some old versions of OCaml did some "singleton promotion", i.e.
[< `A of int] was automatically converted to [`A of int].
This was removed as an unnecessary complication, and also because you
might actually want to distinguish the two for private row types.

Jacques Garrigue

Re: [Caml-list] Difference between [ `A ] and [< `A ]

[Christophe Raffalli]

[-- Attachment #1: Type: text/plain, Size: 1083 bytes --]


> For instance, [<  `A of int] and [< `A of bool] are unifiable, giving [< `A of int & bool],

OK ... this means you can write (I tested in 3.11.2) :

# type ('a,'b,'c) inter = [< `A of 'b & 'c] as 'a;;
type ('a, 'b, 'c) inter = 'a constraint 'a = [< `A of 'b & 'c ]

which seems to be a type isomorphic to the intersection type of 'b and 'c ...

does this mean we can play with intersection type in OCaml (using some type cast because
intersection type is undecidable ...)

In other word : can we encode system D in OCaml ?

Cheers,
Christophe


-- 
Christophe Raffalli
Universite de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tel: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
---------------------------------------------
IMPORTANT: this mail is signed using PGP/MIME
At least Enigmail/Mozilla, mutt or evolution
can check this signature. The public key is
stored on www.keyserver.net
---------------------------------------------


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 262 bytes --]