Browse thread
Oddness with recursive polymorphic variants
-
Jeremy Yallop
-
Nils Gesbert
- Nils Gesbert
- Jeremy Yallop
-
Nils Gesbert
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| From: | Jeremy Yallop <j.d.yallop@s...> |
| Subject: | Re: [Caml-list] Oddness with recursive polymorphic variants |
Thanks for all the replies. My current understanding is as follows:
Given the types
type f = [`A]
type g = [f | `C]
then the following function is not acceptable
let k (x:f) = (x:g)
because f and g are not unifiable: they are "closed rows" with different
fields. There are a number of ways to "open" the row, however:
let k (#f as x:f) = (x:g)
This one is acceptable because the pattern "#f" means "an open row that
includes all the tags in f". (That's its type on the rhs, anyway. The
pattern (and the function) will accept exactly those tags in the type
"f"). The type annotation on the parameter doesn't affect the type of
"x", although the compiler does check that the type of the annotation
and of the pattern can be unified. The case where all the tags (only
one in this case) are enumerated is treated identically:
let k (`A as x:f) = (x:g)
Finally, the explicit coercion (:>). Like the acceptable patterns, this
"opens" the row, allowing it to be unified with "g" (or, indeed, with
any other row type whose tag parameters don't clash with those of "f").
How does that sound?
Jeremy.