Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss

[Caml-list] Question about polymorphic variant

1 view
Skip to first unread message

Jacques Garrigue

unread,
Oct 22, 2002, 8:20:24 PM10/22/02
to raff...@univ-savoie.fr, caml...@inria.fr
From: Christophe Raffalli <raff...@univ-savoie.fr>
> After reading the manual, I am a bit confused ...
> I should say this part of the manual could be clearer ?

Maybe. Let's just say that polymorphic variant typing is a bit
involved...

> In the following code, f and g typecheck but not h.
> Why ?
>
> let f = function
> `a -> 0
> | `b -> 1
>
> let g = function
> `c -> 2
> | (`a | `b as x) -> f x
>
> let h = function
> `c -> 2
> | x -> f x

You must first understand how works type checking for
pattern-matching. Basically the idea is that you have a list of cases
pat1 -> expr1 | ... | patn -> exprn, and that all patterns and all
expressions have their types unified. In h this means that x will get
the same type as `c, i.e. [> `c], and will then be unified to the
input type of f : [< `a|`b] -> int. Since `c is not allowed as input
to f, this fails. (By the way, in ocaml 3.00 h would be accepted, but
with type [< `a|`b] -> int, which is probably nto what you intended.)

The typing of g procedes a bit differently. The type of (`a|`b as x)
will still be [< `a|`b|`c], but the type of x can be restricted to
those actually matched by the pattern it aliases, i.e. [> `a|`b]. As
a result inference succeeds.

Now you might be wondering why in the first place we gave the same
type to all pattern-matching cases. Indeed, if `c is matched first, it
cannot occur anymore in subsequent cases. But the trouble with such an
approach is that it doesn't generalize well: we would need to do
exhaustivity checking before typing, but exhaustivity checking itself
depends on typing. Even limiting ourselves to trivial cases, this
would add to the confusion by adding variables that refer not to
types, but just to bits of types. So we prefer to keep the more
conservative typing rule for pattern-matching, putting rather the
emphasis on dispatch.

Jacques Garrigue
-------------------
To unsubscribe, mail caml-lis...@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

0 new messages