From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id CAA08591; Wed, 23 Oct 2002 02:18:15 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id CAA09255 for ; Wed, 23 Oct 2002 02:18:14 +0200 (MET DST) Received: from favie.faith.gr.jp (favie.faith.gr.jp [61.127.175.250]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id g9N0IC507542 for ; Wed, 23 Oct 2002 02:18:13 +0200 (MET DST) Received: from localhost (dhcp7.faith.gr.jp [192.168.1.17]) by favie.faith.gr.jp (8.9.3/8.9.3) with ESMTP id JAA26870; Wed, 23 Oct 2002 09:18:04 +0900 To: raffalli@univ-savoie.fr Cc: caml-list@inria.fr Subject: Re: [Caml-list] Question about polymorphic variant In-Reply-To: <3DB574DA.5080908@univ-savoie.fr> References: <200210221507.g9MF7b517633@concorde.inria.fr> <3DB574DA.5080908@univ-savoie.fr> X-Mailer: Mew version 1.94.2 on Emacs 21.2 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit Message-Id: <20021023091736F.garrigue@kurims.kyoto-u.ac.jp> Date: Wed, 23 Oct 2002 09:17:36 +0900 From: Jacques Garrigue X-Dispatcher: imput version 20000228(IM140) Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk 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 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-list-request@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