# types and polymorphic variants

# types and polymorphic variants

[Manuel Fahndrich]

What is the meaning of #foo, when foo is a polymorphic variant set?

type foo = [`A | `B | `C]

I assumed that it was the following:

	#foo = [<`A | `B | `C ]

that is a set containing at most `A | `B | `C. In other words a subtype of
foo.

But consider the following example.

type foo = [`A | `B | `C]

let foo1 (x : #foo as 'a) = x

let y1 = foo1 (`A : [`A])


let foo2 (x : [< `A | `B | `C] as 'a) = x

let y2 = foo2 (`A : [`A])


The complier tells me:

ocamlc -c -i ex1.ml

type foo = [`A|`B|`C]
val foo1 : (#foo as 'a) -> 'a
val y1 : foo
val foo2 : ([<`A|`B|`C] as 'a) -> 'a
val y2 : [`A]

The first function returns me only a foo, the second function returns me
[`A] as expected. Thus my question, what exactly does #foo stand for. I do
understand row variables, but the issue with the lower and upper bounds > <
in variant types seems new. Is there a paper describing these?

I seem to write types of the form [< `A | `B | `C] a lot. Shouldn't there be
an abbreviation for those as well? Maybe #<foo?


Thanks in advance for such a wonderfully expressive type system!

	Manuel

Re: # types and polymorphic variants

[Jacques Garrigue]

From: Manuel Fahndrich <maf@microsoft.com>

> What is the meaning of #foo, when foo is a polymorphic variant set?
> 
> type foo = [`A | `B | `C]
> 
> I assumed that it was the following:
> 
> 	#foo = [<`A | `B | `C ]
> 
> that is a set containing at most `A | `B | `C. In other words a subtype of
> foo.

This is correct. Notice however that [> `A | `B | `C] would also be a
subtype of foo (although from a different point of view), so there is
a choice done here between two possibilities, and I took the seemingly
most useful/intuitive.

> But consider the following example.
[...]

It seems that you found a bug in ocaml-2.99. If you are particularly
interested in variants, I suggest you switch to the CVS version.

With the current CVS version it works as you expect:

        Objective Caml version 2.99+6 (2000/02/25)

# type foo = [`A|`B|`C];;
type foo = [`A|`B|`C]
# let foo1 (x : #foo) = x;;
val foo1 : (#foo as 'a) -> 'a = <fun>
# let y1 = foo1 (`A : [`A]);;
val y1 : [`A] = `A
# let foo2 (#foo as x) = x;;
val foo2 : #foo -> [>`A|`B|`C] = <fun>
# foo2 (`A : [`A]);;
- : _[>`A|`B|`C] = `A

foo2 shows the difference between the type #foo, and the pattern #foo,
which intuitively accepts all values of type #foo, but also permits
type refinement when combined with "as".

> The first function returns me only a foo, the second function returns me
> [`A] as expected. Thus my question, what exactly does #foo stand for. I do
> understand row variables, but the issue with the lower and upper bounds > <
> in variant types seems new. Is there a paper describing these?

The answer is that your intuition was correct.
You will find a description of variants in "Programming with polymorphic
variants", ML Workshop '98, Baltimore. You can get it from my home
page.
In fact the system in ocaml 3 is a refinement of that, forgetting the
type of a tag when it disappears from the upper bound, but this
shouldn't matter in most cases.

Jacques
---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>