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