Type constraints

Type constraints

[Ernesto Posse]

[My apologies for not including a French Version]

Hello. I have the folowing problem. I need to define some interrelated
types as follows:

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

The interpreter prints the inferred type:

type 'a node = { x: 'a; y: t1 } constraint 'a = string * t2
type t1 = | A | B of t1 * t1
type t2 = | C | D of (string * t2) node

Now, if I add another constructor:

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

A solution to this would be something like:

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

This works, but I am not sure to understand the type clash in the former
example. Why did the type synthetizer infer that constraint?

Thank you for any insights on this.

-- 
Ernesto Posse
Ingeniero de Sistemas y Computacion
(Systems and Computing Engineer)
Universidad de los Andes
Santafe de Bogota
Colombia
e-mail: mposada@impsat.net.co

Type constraints

[Pascal Brisset]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 852 bytes --]

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

Re: Type constraints

[Didier Rousseau]

bonjour a tous,


Ernesto Posse wrote:
> 
> [My apologies for not including a French Version]
> 
> Hello. I have the folowing problem. I need to define some interrelated
> types as follows:
> 
> type 'a node = {x: 'a; y: t1}
> and t1 = A | B of t1*t1
> and t2 = C | D of (string * t2) node
> 
> The interpreter prints the inferred type:
> 
> type 'a node = { x: 'a; y: t1 } constraint 'a = string * t2
> type t1 = | A | B of t1 * t1
> type t2 = | C | D of (string * t2) node
> ...


une solution est de declarer :

type 'a node = {x: 'a; y: t1}
and t1 = A | B of t1*t1
;;

type t2 = C | D of (string * t2) node | E of bool node
;;




Didier Rousseau

Re: Type constraints

[Vale'rie Me'nissier-Morain]

Why do you need to define t2 simultaneously to 'a node and t1?

The following session is ok in Caml Light

>       Caml Light version 0.73

#type 'a node = {x: 'a; y: t1}
and t1 = A | B of t1*t1;;
Type node defined.
Type t1 defined.
#type t2 = C | D of (string * t2) node;;
Type t2 defined.
#type t2 = C | D of (string * t2) node | E of bool node;;
Type t2 defined.
#

or, if you prefer in Objective Caml

        Objective Caml version 1.05

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

V. Ménissier-Morain

Re: Type constraints

[Wolfgang Lux]

> Hello. I have the folowing problem. I need to define some interrelated
> types as follows:
> 
> type 'a node = {x: 'a; y: t1}
> and t1 = A | B of t1*t1
> and t2 = C | D of (string * t2) node
> 
> The interpreter prints the inferred type:
> 
> type 'a node = { x: 'a; y: t1 } constraint 'a = string * t2
> type t1 = | A | B of t1 * t1
> type t2 = | C | D of (string * t2) node
> 

A simple solution to get rid of the type constraint in this case, is to 
reorder the type definitions as follows:

type t1 = A | B of t1*t1
type 'a node = {x: 'a; y: t1}
type t2 = C | D of (string * t2) node

> Now, if I add another constructor:
> 
> 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
> 
> A solution to this would be something like:
> 
> type ('a,'b) node = {x: 'a; y: 'b}
> and t1 = A | B of t1*t1
> and t2 = C | D of (string * t2, t1) node | E of (bool, t1) node
> 
> This works, but I am not sure to understand the type clash in the former
> example. Why did the type synthetizer infer that constraint?

I'm not absolutely sure on this, but it looks just like another case of 
the monomorphic recursion restriction of the Hindley-Milner type system.
 
> 
> Thank you for any insights on this.
> 

Hope this helps.

Regards
Wolfgang

----
Wolfgang Lux                     WZH Heidelberg, IBM Germany
Phone: +49-6221-59-4546                Fax: +49-6221-59-3500
Internet: lux@heidelbg.ibm.com          Office: mazvm01(lux)

Re: Type constraints

[Jerome Vouillon]

On Thu, 29 May 1997, Ernesto Posse wrote:

> 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

In the current release, in mutually recursive type definitions, all
occurrences of a type being defined (here, for instance, 'a node) must
have the same parameters.
This overly restrictive constraint will be removed in the next
release.  In the meantime, as Didier Rousseau noticed, you can move
the definition of type t2 out of the recursive type definition: 

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

-- Jerome Vouillon

Type constraints

[Jim Farrand]

Hi,

I am writing a camlp4 extension to implement dynamic types in O'Caml[1].
I am doing this by generating run-time type representations of values.
When a value is "made dynamic" I tag it with type information.  Then
when it is later "made static" I check the tagged type information
against the type the value is being cast to.

(* x is a dynamic value with type Dynamic.t *)
value x = (10 => dynamic int) ; 

(* y has type int. *)
value y = (x => static int) ;

(* y has type string *)
value z = (x => static string) ;
(* (But as x doesn't have an int, this raises a Type_error exception) *)

When generating the code for the first example, I have to check that x
really has type int, so that the run-time type information I output
matches the actual type..  I do this by introducing a type constraint.

(x : int)

This works fine for monomorphic value, but I now want to extend to
polymorphic values.  The idea is that if you have a value, which has a
polymorphic type, eg.

value x = ((fun x -> x) => dynamic 'a -> 'a) ;

The problem is that the type constraint generated,

((fun x -> x) : 'a -> 'a)

does not reject values with a less general type.  This is fine when the
type given matches the function, as it does above, but causes me
problems if the type given is less general.

For example,

value x = ((fun x -> x) => dynamic 'a -> int) ;

yields

((fun x -> x) : 'a -> int)

which is happily compiled by ocaml (I want to reject it).

(To understand why this is a problem, consider the code

value y = (x => static 'a -> int) ;

My extension will accept this as the type matches the type given when
the value was made dynamic.  I can now do

value z = y "foo" ; (** Ooops! Just cast a string to an int!! *)

How can I achieve this?

It occurs to me that if I declared a record with a polymorphic type

{ foo : ! 'a . 'a -> 'a }

then values with the intended type are accepted

value t = { foo = id } 

wherease values with a less general type are not

value t = { foo = (id : 'a -> int) } ; (** Type error *)

It seems logical to me that I should be able to use similar syntax in
type constraints, eg. (id : ! 'a . 'a -> 'a), and I think that if I
could, I could use this to solve my problems.

        Objective Caml version 3.09+dev3 (2004-10-06)

# #load "camlp4r.cma" ;;

        Camlp4 Parsing version 3.09+dev3 (2004-10-06)

# value id x = x ;
value id : 'a -> 'a = <fun>
# (id : ! 'a . 'a -> 'a) ;
This expression has type 'a -> 'a but is here used with type 'b. 'b ->
'b

Why is this?

Thanks in advance, and sorry for such a long post.
Jim

[1] I know that there are all sorts of reasons why I shouldn't be doing
this.  I'm not arguing that it's a good idea, but it's certainly
interesting.
-- 
Jim Farrand