Type constraints

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

Re: [Caml-list] Type constraints

[Alain Frisch]

Jim Farrand wrote:
> Hi,

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

Maybe you can use local structures and signatures:

(e :: s)  ==>
let module M : sig val v : s end = struct let v = e end in M.v;;

where s is a type scheme.

Btw, does someone know why in

# let module M : sig val v: 'a -> 'a end = struct let v x = x end in M.v;;
- : '_a -> '_a = <fun>

the type variable is not generalized ?


-- Alain

Re: [Caml-list] Type constraints

[Damien Doligez]

On 7 Dec 2004, at 08:12, Alain Frisch wrote:

> Btw, does someone know why in
>
> # let module M : sig val v: 'a -> 'a end = struct let v x = x end in 
> M.v;;
> - : '_a -> '_a = <fun>
>
> the type variable is not generalized ?

Consider this:

   let module M = struct let v = ref end in M.v;;

-- Damien

Re: [Caml-list] Type constraints

[Andreas Rossberg]

Damien Doligez wrote:
> On 7 Dec 2004, at 08:12, Alain Frisch wrote:
> 
>> Btw, does someone know why in
>>
>> # let module M : sig val v: 'a -> 'a end = struct let v x = x end in 
>> M.v;;
>> - : '_a -> '_a = <fun>
>>
>> the type variable is not generalized ?
> 
> Consider this:
> 
>   let module M = struct let v = ref end in M.v;;

Is this really a counter-example? I don't see any problem with making it 
polymorphic - it evaluates to ref, and ref can happily be polymorphic.

	- Andreas

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

Let's get rid of those possible thingies!  -- TB

Re: [Caml-list] Type constraints

[Damien Doligez]

On 7 Dec 2004, at 15:57, Andreas Rossberg wrote:

> Is this really a counter-example? I don't see any problem with making 
> it polymorphic - it evaluates to ref, and ref can happily be 
> polymorphic.

Yes, well I simplified it a bit too much.  Try this instead:

   let module M = struct let v = ref [] end in M.v;;

-- Damien

Re: [Caml-list] Type constraints

[Alain Frisch]

Damien Doligez wrote:
> Yes, well I simplified it a bit too much.  Try this instead:
> 
>   let module M = struct let v = ref [] end in M.v;;

I still don't understand. Compare:

# module M = struct let v = ref [] end;;
module M : sig val v : '_a list ref end
# module M : sig val v : 'a -> 'a end = struct let v x = x end;;
module M : sig val v : 'a -> 'a end

Of course, the type variable in the first example must not be 
generalized, and it isn't. In the second example, there is no problem. 
We get:

# M.v;;
- : 'a -> 'a = <fun>

So why not give the same type scheme to:

let module M : sig val v : 'a -> 'a end = struct let v x = x end in M.v

?


Alain

Re: [Caml-list] Type constraints

[Damien Doligez]

On 7 Dec 2004, at 19:08, Alain Frisch wrote:

> I still don't understand. Compare:
>
> # module M = struct let v = ref [] end;;
> module M : sig val v : '_a list ref end
> # module M : sig val v : 'a -> 'a end = struct let v x = x end;;
> module M : sig val v : 'a -> 'a end
>
> Of course, the type variable in the first example must not be 
> generalized, and it isn't. In the second example, there is no problem. 
> We get:
>
> # M.v;;
> - : 'a -> 'a = <fun>
>
> So why not give the same type scheme to:
>
> let module M : sig val v : 'a -> 'a end = struct let v x = x end in M.v

The typing algorithm is very simple (really!):

1. Type the module. Generalization occurs and the v field gets a
    polymorphic type.
2. Type "M.v".  This takes an instance of the polymorphic type.
3. Can we generalize it?  Look at the syntactic shape of the expression
    (in this case, let module ... in ...).  If it is always safe to
    generalize such expressions, OK.  If not, do not generalize.

That's the beauty of the Wright criterion: it's very easy to implement
and to understand (because it is syntactic), and works well in almost 
all
cases (with a little eta-expansion if needed).

So the answer to your original question is: the type is not generalized
because in some cases the let-module construct is not safely 
polymorphic.

Of course, there must be some criteria for generalizing more
expressions.  Check out Xavier's thesis for example.  They are usually
not worth the trouble.

-- Damien

Re: [Caml-list] Type constraints

[Alain Frisch]

Damien Doligez wrote:

> So the answer to your original question is: the type is not generalized
> because in some cases the let-module construct is not safely polymorphic.

Ah ok, this explains that:

# let module M = struct end in fun x -> x;;
- : '_a -> '_a = <fun>

Still, I'm not sure to understand the bottomline. Consider:

# module M = struct let v = ref [] end;;
module M : sig val v : '_a list ref end
# M.v;;
- : '_a list ref = {contents = []}

Here M.v is not generalized either. But here it is:

# module M = struct let v x = x end;;
module M : sig val v : 'a -> 'a end
# M.v;;
- : 'a -> 'a = <fun>

So I don't understand why the same cannot apply to local modules. If the 
let-module-in were declared "safe" for the value restriction, shouldn't

let module M = struct let v = ref [] end in M.v

yield a non-generalized type for the same reason as for the non-local
case (and not because of the value restriction) ?


-- Alain

Re: [Caml-list] Type constraints

[nakata keiko]

Damien Doligez wrote:

>The typing algorithm is very simple (really!):
>
>1. Type the module. Generalization occurs and the v field gets a
>    polymorphic type.
>2. Type "M.v".  This takes an instance of the polymorphic type.
>3. Can we generalize it?  Look at the syntactic shape of the expression
>    (in this case, let module ... in ...).  If it is always safe to
>    generalize such expressions, OK.  If not, do not generalize.
>
>That's the beauty of the Wright criterion: it's very easy to implement
>and to understand (because it is syntactic), and works well in almost 
>all
>cases (with a little eta-expansion if needed).

This does not answer to me why this works,

#type t = { t : 'a. 'a -> 'a}

#let v = let module M = struct let t x = x end in {t = M.t} in (v.t 5, v.t true)

Of cource, both of the following are not type checked,

#let v = let module M = struct let  t = x end in  M.t in (v 5, v true)

#let v : 'a -> 'a = let module M = struct let t x = x end in  M.t in (v 5, v true)

However, if I can write something like

#let v : 'a. 'a -> 'a = let module M = struct let t x = x end in  M.t in (v 5, v true)

then, it would be type checked ?

Regards,
Keiko.

Re: [Caml-list] Type constraints

[nakata keiko]

Damien Doligez wrote:
> On 8 Dec 2004, at 04:30, nakata keiko wrote:
> 
> > This does not answer to me why this works,
> >
> > #type t = { t : 'a. 'a -> 'a}
> >
> > #let v = let module M = struct let t x = x end in {t = M.t} in (v.t 5, 
> > v.t true)
> 
> You'll have to ask Jacques about this.  He's the one who added 
> polymorphic
> methods and polymorphic record labels to the language, and I'm not sure
> I understand all the implications.

I have the impression that if the above code is type checked,
then, something like the following code could be type checked.
What is the differences?

> > However, if I can write something like
> >
> > #let v : 'a. 'a -> 'a = let module M = struct let t x = x end in  M.t 
> > in (v 5, v true)
> >
> > then, it would be type checked ?
> 
> I doubt it.  For the moment, a type constraint can only specialize the
> type of an expression.  You're asking for a generalization constraint.
> I have no idea whether that can be implemented, but I think it would
> require some big changes to the typechecker.

Regards,
Keiko.

Re: [Caml-list] Type constraints

[Jacques Garrigue]

From: nakata keiko <keiko@kaba.or.jp>

> > > This does not answer to me why this works,
> > >
> > > #type t = { t : 'a. 'a -> 'a}
> > >
> > > #let v = let module M = struct let t x = x end in {t = M.t} in (v.t 5, 
> > > v.t true)
> 
> I have the impression that if the above code is type checked,
> then, something like the following code could be type checked.
> What is the differences?
> 
> > > #let v : 'a. 'a -> 'a = let module M = struct let t x = x end in  M.t 
> > > in (v 5, v true)

These two examples use different kinds of polymorphism.
In the first case, the data structure ensures the polymorphism,
meaning that even if the type of the data structure is made
non-generalizable, you can still extract a polymorphic value from it
later.
That's why you can pass such values to functions, and use them
polymorphically inside (which you cannot do with normal variables.)

A simple example of the difference is
   (fun v -> (v.t 5, v.t true)) {t = fun x -> x}
vs.
   (fun v -> (v 5, v true)) (fun x -> x)

There is currently no way to make a first-class polymorphic value in
ocaml without using either record or object.
(There is no theoretical limitation, just we could never come up with
the right syntax for introduction and elimination.)

Jacques Garrigue

Re: [Caml-list] Type constraints

[Damien Doligez]

On 7 Dec 2004, at 22:43, Alain Frisch wrote:

> Damien Doligez wrote:
>
>> So the answer to your original question is: the type is not 
>> generalized
>> because in some cases the let-module construct is not safely 
>> polymorphic.

[...]

> So I don't understand why the same cannot apply to local modules. If 
> the let-module-in were declared "safe" for the value restriction, 
> shouldn't
>
> let module M = struct let v = ref [] end in M.v
>
> yield a non-generalized type for the same reason as for the non-local
> case (and not because of the value restriction) ?

Hmmm...  Now I don't know whether it's safe or not, and I don't know
whether someone checked its safety before excluding it from the value
restriction code...

-- Damien

Re: [Caml-list] Type constraints

[Alain Frisch]

Damien Doligez wrote:
> Hmmm...  Now I don't know whether it's safe or not, and I don't know
> whether someone checked its safety before excluding it from the value
> restriction code...

With this extra line added to is_nonexpansive:

   | Texp_letmodule (_,_,e) -> is_nonexpansive e

we get:

# let module M = struct let x = ref [] end in M.x;;
- : 'a list ref = {contents = []}

The non-generalizable status has been forgotten. What I'm not sure is 
whether this is only an artefact of the internal representation of 
levels to control generalization, or whether there are some deeper issues.


-- Alain

Re: [Caml-list] Type constraints

[Jacques Garrigue]

From: Alain Frisch <Alain.Frisch@inria.fr>
> Damien Doligez wrote:
> > Hmmm...  Now I don't know whether it's safe or not, and I don't know
> > whether someone checked its safety before excluding it from the value
> > restriction code...
> 
> With this extra line added to is_nonexpansive:
> 
>    | Texp_letmodule (_,_,e) -> is_nonexpansive e
> 
> we get:
> 
> # let module M = struct let x = ref [] end in M.x;;
> - : 'a list ref = {contents = []}
> 
> The non-generalizable status has been forgotten. What I'm not sure is 
> whether this is only an artefact of the internal representation of 
> levels to control generalization, or whether there are some deeper issues.

It's not really an artefact, just that there is no such thing as a
non-generalizable status: something that is not generalizable in some
context becomes generalizable in a larger context.
So you cannot rely on the generalizability obtained during the typing
of the module. Rather you must check whether the module
itself contains only non-expansive definitions. I.e. you cannot ignore
the definition of the module, as you are doing here.

Yet, modules are strange beasts for typing, so I wouldn't add the code
before thinking it through.

(Note that there is another way to handle non-generalizability,
without relying on a non-expansiveness predicate, raising the
non-generalizable level only when entering functions, and that might
solve the problem for free. Francois Pottier told me he was using
it. However it requires many small changes to type inference, and
doesn't mix well with the new "relaxed" value restriction.)

Jacques Garrigue

Re: [Caml-list] Type constraints

[skaller]

On Thu, 2004-12-09 at 01:23, Jacques Garrigue wrote:

> Yet, modules are strange beasts for typing, so I wouldn't add the code
> before thinking it through.

I am curious as to the status of COQ support for verifying
assertions about proposed changes to the type system.

For example supposing you did 'think it through' and it
seemed right, would you be able to then extend an
existing COQ proof and attempt to prove your thinking
mechanically?

-- 
John Skaller, mailto:skaller@users.sf.net
voice: 061-2-9660-0850, 
snail: PO BOX 401 Glebe NSW 2037 Australia
Checkout the Felix programming language http://felix.sf.net

Re: [Caml-list] Type constraints

[Jacques Garrigue]

From: skaller <skaller@users.sourceforge.net>
> On Thu, 2004-12-09 at 01:23, Jacques Garrigue wrote:
> 
> > Yet, modules are strange beasts for typing, so I wouldn't add the code
> > before thinking it through.
> 
> I am curious as to the status of COQ support for verifying
> assertions about proposed changes to the type system.
> 
> For example supposing you did 'think it through' and it
> seemed right, would you be able to then extend an
> existing COQ proof and attempt to prove your thinking
> mechanically?

Unfortunately, I'm afraid we are still pretty far from that.
Supposing we could describe all the properties we need in Coq
(probably possible, but far from easy), a very long and harduous
proof is waiting.
If there is a breakthrough, I would be most happy to check everything,
as I know there are bugs in the compiler. I just discovered a stupid
unsoundness today.

Jacques Garrigue

Re: [Caml-list] Type constraints

[Xavier Leroy]

> Hmmm...  Now I don't know whether it's safe or not, and I don't know
> whether someone checked its safety before excluding it from the value
> restriction code...

You word it in a slightly backward way: it is always safe to claim
that an expression is expansive and its type should not be
generalized; it's the converse (asserting that an expression is
non-expansive) that is potentially dangerous and requires some
semantic evidence that it is safe.  The current treatment of "let
module" as being always expansive just errs on the safe side, in the
absence of this semantic evidence.

> >So I don't understand why the same cannot apply to local modules. If 
> >the let-module-in were declared "safe" for the value restriction, 
> >shouldn't
> >
> >let module M = struct let v = ref [] end in M.v
> >
> >yield a non-generalized type for the same reason as for the non-local
> >case (and not because of the value restriction) ?

I don't follow you here.  So, OK, your expression E above
(E = let module M = struct let v = ref [] end in M.v) has type
alpha list ref for a fresh variable alpha.  If we were to classify E
as non-expansive, we could do 

      let x = E in E'

and in E', x would have polymorphic type forall alpha, alpha list ref,
from which it is easy to break type safety.

So, your example shows that it would be unsafe to say that a "let
module M = A in B" expression is nonexpansive if B is nonexpansive.
One would need to inspect the module expression A to establish that it
is nonexpansive.  This is what we do for ordinary "let" expressions:
"let x = A in B" is nonexpansive if both A and B are nonexpansive.

There are two concerns here.  The practical one is that the module
language is quite complex and I really don't feel like implementing a
syntactic nonexpansiveness check for module expressions.  

The conceptual concern is that the type system for the module language
is somewhat richer than that of the core language -- it has "deep"
polymorphism, subtyping and some forms of dependent types -- so it is
not entirely clear to me that the value restriction and the syntactic
nonexpansiveness criterion that work for the core language would also
work for the module language.

- Xavier Leroy

Re: [Caml-list] Type constraints

[William Lovas]

On Tue, Dec 07, 2004 at 06:44:36PM +0100, Damien Doligez wrote:
> 
> On 7 Dec 2004, at 15:57, Andreas Rossberg wrote:
> 
> >Is this really a counter-example? I don't see any problem with making 
> >it polymorphic - it evaluates to ref, and ref can happily be 
> >polymorphic.
> 
> Yes, well I simplified it a bit too much.  Try this instead:
> 
>   let module M = struct let v = ref [] end in M.v;;

I'm still not convinced.  Yes, the type variable should not be generalized
in the above, by analogy with:

    # ref [];;
    - : '_a list ref = {contents = []}

But the `let module' in question -- or one similar in spirit, at least --

    # let module M = struct let v = fun x -> x end in M.v;;
    - : '_a -> '_a = <fun>

is analogous to the expression

    # fun x -> x
    - : 'a -> 'a = <fun>

in which the type variable *is* generalized.

The following behavior confuses me, too:

    # let module M = struct let v = fun x -> x end in (M.v 5, M.v true);;
    - : int * bool = (5, true)
    This expression has type bool but is here used with type int
    # let v =
        let module M = struct let v = fun x -> x end in M.v
      in
        (v 5, v true);;
                ^^^^
    This expression has type bool but is here used with type int

Why is the type variable generalized inside the `let module's body but not
generalized if we pass it to the outside?

So the `ref' example above as a counterexample is at the very least hiding
some of the story.  What's really going on here?

William

Re: [Caml-list] Type constraints

[Jacques Garrigue]

From: William Lovas <wlovas@stwing.upenn.edu>

> On Tue, Dec 07, 2004 at 06:44:36PM +0100, Damien Doligez wrote:
> > 
> > On 7 Dec 2004, at 15:57, Andreas Rossberg wrote:
> > 
> > >Is this really a counter-example? I don't see any problem with making 
> > >it polymorphic - it evaluates to ref, and ref can happily be 
> > >polymorphic.
> > 
> > Yes, well I simplified it a bit too much.  Try this instead:
> > 
> >   let module M = struct let v = ref [] end in M.v;;
> 
> I'm still not convinced.  Yes, the type variable should not be generalized
> in the above, by analogy with:
> 
>     # ref [];;
>     - : '_a list ref = {contents = []}
> 
> But the `let module' in question -- or one similar in spirit, at least --
> 
>     # let module M = struct let v = fun x -> x end in M.v;;
>     - : '_a -> '_a = <fun>
> 
> is analogous to the expression
> 
>     # fun x -> x
>     - : 'a -> 'a = <fun>
> 
> in which the type variable *is* generalized.

Analogies don't help you here, because the typechecker doesn't work by
analogies, but by explicit rules.
If you're curious, there is a function is_nonexpansive in
typing/typecore.ml. Only expressions for which this function returns
true will be generalized. (This is a direct implementation of the
syntactic value-generalization scheme.)
Now, this function doesn't now about Texp_letmodule, so any use of
this construct will never be generalized. I don't know exactly why
this was omitted, but I see the combination of two possible reasons:
this requires some amount of extra code, and one must assess its
validity. Yet I suppose this could be done.
By the way, the code is already there for immediate objects, so the
alternative approach with polymorphic methods does work (but generates
more code).

# let o = object method v : 'a. 'a -> 'a = fun x -> x end in
  fun x -> o#v x;;
- : 'a -> 'a = <fun>

Jacques Garrigue

Re: [Caml-list] Type constraints

[Boris Yakobowski]

On Tue, Dec 07, 2004 at 06:44:36PM +0100, Damien Doligez wrote:
> 
> On 7 Dec 2004, at 15:57, Andreas Rossberg wrote:
> 
> >Is this really a counter-example? I don't see any problem with making 
> >it polymorphic - it evaluates to ref, and ref can happily be 
> >polymorphic.
> 
> Yes, well I simplified it a bit too much.  Try this instead:
> 
>   let module M = struct let v = ref [] end in M.v;;

The question remains : why not generalize type variables which would be
generalized at the end of a non local module? :

# module M = struct let v = ref [] end;;
module M : sig val v : '_a list ref end
# module M = struct let v x = x end;;
module M : sig val v : 'a -> 'a end
# let module M = struct let v = ref [] end in M.v;;
- : '_a list ref = {contents = []}
# let module M = struct let v x = x end in M.v
(* This seems overly restrictive *);;
- : '_a -> '_a = <fun>

Besides:
# type t = {t : 'a. 'a -> 'a};;
type t = { t : 'a. 'a -> 'a; }
# let module M = struct let v x = x end in { t = M.v };;
- : t = {t = <fun>}

-- 
Boris

Re: [Caml-list] Type constraints

[Jim Farrand]

On Tue, Dec 07, 2004 at 08:12:20AM +0100, Alain Frisch wrote:

> Maybe you can use local structures and signatures:
> (e :: s)  ==>
> let module M : sig val v : s end = struct let v = e end in M.v;;

Thanks for this, I haven't had chance to code it up yet but suspect it
is exactly the solution I was looking for.

Thanks also to those who replied off list with similar hints.

REgards,
Jim

-- 
Jim Farrand

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