Type constraints

From: Pascal Brisset (brisset@recherche.enac.fr)
Date: Fri May 30 1997 - 09:41:10 MET DST

Message-Id: <199705300741.JAA23620@indigo.recherche.enac.fr>
Date: Fri, 30 May 1997 09:41:10 +0200
From: Pascal Brisset <brisset@recherche.enac.fr>
To: caml-list@pauillac.inria.fr
Subject: Type constraints
In-Reply-To: <338DD17B.62C6@impsat.net.co>

Ernesto Posse writes:
type 'a node = {x: 'a; y: t1}
and t1 = A | B of t1*t1
and t2 = C | D of (string * t2) node | E of bool node

I obtain this message:

Characters 98-102:
This type parameter bool should be an instance of type string * t2

It may be compared to a similar expression at the term level:

# let rec f = fun x -> x
  and g = f 1, f "1";;
This expression has type string but is here used with type int

In a recursive definition, occurrences of the defined idents have the
same type everywhere, i.e. the generalization (in your case, 'a is any
type) is done only ``at the end'' of the definition.

At the term level, ML+ is the (undecidable) solution to this kind of
recursive definition. I guess problems are similar at the type level.

A more precise answer from a Caml guru ?

--Pascal Brisset

This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:11 MET