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 KAA17413; Tue, 10 Apr 2001 10:21:52 +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 KAA17409 for ; Tue, 10 Apr 2001 10:21:51 +0200 (MET DST) Received: from quincy.inria.fr (quincy.inria.fr [128.93.8.52]) by concorde.inria.fr (8.11.1/8.10.0) with ESMTP id f3A8Lnb15510 for ; Tue, 10 Apr 2001 10:21:49 +0200 (MET DST) Received: (from mauny@localhost) by quincy.inria.fr (8.10.1/8.10.1) id f3A8NN813340 for caml-list@inria.fr; Tue, 10 Apr 2001 10:23:23 +0200 Date: Tue, 10 Apr 2001 10:23:23 +0200 From: Michel Mauny To: caml-list@inria.fr Subject: Re: [Caml-list] variant with tuple arg in pattern match? Message-ID: <20010410102323.A13306@quincy.inria.fr> Reply-To: Michel.Mauny@inria.fr References: <200104091607.SAA03671@pauillac.inria.fr> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline User-Agent: Mutt/1.2.5i In-Reply-To: <200104091607.SAA03671@pauillac.inria.fr>; from Pierre.Weis@inria.fr on Mon, Apr 09, 2001 at 06:07:16PM +0200 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk On Sun, 8 Apr 2001, Pierre Weis wrote: > I suggest to explicitely annotate the constructor definitions as in: > > type t = > | C : int -> int -> t > This notation is explicit, intuitive, and allows refined type checking > in some cases (for instance > type 'a t = C : int -> bool -> (int * bool) t). Alain Frish then asked: > How does this interact with pattern matching ? Pierre Weis replied: > As usual. There would be no interaction with the pattern matching > facility of Objective Caml. Well, as far as I understand, there is an interaction with pattern-matching. Consider the following example: type 'a t = Int : int -> int t | Bool : bool -> bool t | Node : 'a t -> 'a t -> 'a t This definition implies that data constructors Int and Bool cannot appear in the same tree (no way to be at the same time an int t, and a bool t, unless being an 'a t, which cannot occur at all). Consider now the following traversal function scheme: let rec traverse t = match t with Int n -> ... (* case 1 *) | Bool b -> ... (* case 2 *) | Node t1 t2 -> ... It's a total function, but untypable. If you want to make it typable (and still semantically total), you'd have to suppress either case 1 or case 2. But now, how the compiler will see that the function is indeed total? This is yet another case where the pattern-matching compiler needs to use a non-trivial knowledge from the typechecker. This is indeed understandable, since values of type t are either int t or bool t, that is [int | bool] t, which is pretty close to a feature of variants. -- Michel ------------------- To unsubscribe, mail caml-list-request@inria.fr. Archives: http://caml.inria.fr