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 LAA19498; Tue, 10 Apr 2001 11:14:28 +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 LAA19494 for <caml-list@pauillac.inria.fr>; Tue, 10 Apr 2001 11:14:28 +0200 (MET DST)
Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35])
	by concorde.inria.fr (8.11.1/8.10.0) with ESMTP id f3A9EQb18017;
	Tue, 10 Apr 2001 11:14:26 +0200 (MET DST)
Received: (from xleroy@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id LAA19487; Tue, 10 Apr 2001 11:14:26 +0200 (MET DST)
Date: Tue, 10 Apr 2001 11:14:26 +0200
From: Xavier Leroy <Xavier.Leroy@inria.fr>
To: Michel Mauny <Michel.Mauny@inria.fr>
Cc: caml-list@inria.fr
Subject: Re: [Caml-list] variant with tuple arg in pattern match?
Message-ID: <20010410111426.C16732@pauillac.inria.fr>
References: <Pine.GSO.4.04.10104090209230.4374-100000@clipper.ens.fr> <200104091607.SAA03671@pauillac.inria.fr> <20010410102323.A13306@quincy.inria.fr>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Mailer: Mutt 1.0i
In-Reply-To: <20010410102323.A13306@quincy.inria.fr>; from Michel.Mauny@inria.fr on Tue, Apr 10, 2001 at 10:23:23AM +0200
Sender: owner-caml-list@pauillac.inria.fr
Precedence: bulk

> 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.

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
pattern-matching 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 non-regular 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 non-regular definitions are very useful, e.g. to
express inference rules.)

- Xavier Leroy
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr