[Camllist] variant with tuple arg in pattern match?
[
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:  20010410 (09:14) 
From:  Xavier Leroy <Xavier.Leroy@i...> 
Subject:  Re: [Camllist] variant with tuple arg in pattern match? 
> Well, as far as I understand, there is an interaction with > patternmatching. 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. The Coq proof assistant doesn't agree with you here. (Note to the readers: I'm bringing Coq in the discussion because the notation suggested by Pierre is the one Coq uses for its inductive definitions, which generalize ML datatype definitions.) Inductive t : Set > Set := Int : nat > (t nat)  Bool : bool > (t bool)  Node : (A: Set) (t A) > (t A) > (t A). Definition traverse := [A:Set][x: (t A)] Cases x of (Int _) => O  (Bool _) => (S O)  (Node _ _ _) => (S (S O)) end. Coq gives "traverse" the type (A:Set)(t A)>nat, i.e. 'a t > int in ML syntax. How Coq does this is a bit of a mystery to me, but clearly it doesn't unify the types of the l.h.s. of the patternmatching as we are used to do in ML... Coming back to Pierre's suggestion, I don't see the point in switching to the Coq syntax for declaring datatypes. For one thing, it is considerably more verbose: one has to repeat "> (params) t" at the end of each constructor declaration. For another thing, it allows more nonregular definitions (like Alain Frisch noted) which we don't quite know how to handle, and are useless in practice (in my opinion). Lastly, why change something that works? (For Coq, the situation is different because inductive definitions can define not only data structures, but also logical predicates, and in the latter case the nonregular definitions are very useful, e.g. to express inference rules.)  Xavier Leroy  To unsubscribe, mail camllistrequest@inria.fr. Archives: http://caml.inria.fr