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] does ocaml have a wxWindows classes wraper
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Jacques Garrigue <garrigue@k...>
Subject: Re: [Caml-list] Question about polymorphic variant
From: Christophe Raffalli <>
> 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

> 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 Archives:
Bug reports: FAQ:
Beginner's list: