Re: [Caml-list] variant with tuple arg in pattern match?

[Xavier Leroy <Xavier.Leroy@inria.fr>]

> 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