Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

parameterized recursive types broken #2433

Closed
vicuna opened this issue Apr 28, 2000 · 6 comments
Closed

parameterized recursive types broken #2433

vicuna opened this issue Apr 28, 2000 · 6 comments
Labels

Comments

@vicuna
Copy link

vicuna commented Apr 28, 2000

Original bug ID: 95
Reporter: administrator
Status: closed
Resolution: fixed
Priority: normal
Severity: minor
Category: ~DO NOT USE (was: OCaml general)

Bug description

Full_Name: Manuel Fahndrich
Version: 3.00
OS: win2000
Submission from: tide78.microsoft.com (131.107.3.78)

type a = int collection
and b = string collection
and 'a collection = 'a list
;;

yields:

This type string should be an instance of type int

where "this type" refers to the "string" argument in 'b' definition.

Look like the compiler does not treat collection as a properly parameterized
type.

-Manuel

@vicuna
Copy link
Author

vicuna commented Apr 28, 2000

Comment author: administrator

Sure, the example is simple and can be written differently. That wasn't the
point.

It's simply broken and worked before (in 2.02).

-Manuel

P.S. It's also broken in 2.99

-----Original Message-----
From: Daniel de Rauglaudre [mailto:daniel.de_rauglaudre@inria.fr]
Sent: Friday, April 28, 2000 12:07 PM
To: Manuel Fahndrich
Cc: caml-bugs@pauillac.inria.fr
Subject: Re: parameterized recursive types broken (#2433)

On Fri, Apr 28, 2000 at 08:39:42PM +0200, maf@microsoft.com wrote:

type a = int collection
and b = string collection
and 'a collection = 'a list
;;

yields:

This type string should be an instance of type int

You can write it like this:

type 'a collection = 'a list;;
type a = int collection
and b = string collection;;

You have a similar problem when you write:
let rec a x = f (x + 1)
and b x = f (x ^ "aa")
and f x = x;;

where f is not generalized. But you can write:
let rec f x = x;;
let rec a x = f (x + 1)
and b x = f (x ^ "aa");;

--
Daniel de RAUGLAUDRE
daniel.de_rauglaudre@inria.fr
http://cristal.inria.fr/~ddr/

@vicuna
Copy link
Author

vicuna commented Apr 28, 2000

Comment author: administrator

On Fri, Apr 28, 2000 at 08:39:42PM +0200, maf@microsoft.com wrote:

type a = int collection
and b = string collection
and 'a collection = 'a list
;;

yields:

This type string should be an instance of type int

You can write it like this:

type 'a collection = 'a list;;
type a = int collection
and b = string collection;;

You have a similar problem when you write:
let rec a x = f (x + 1)
and b x = f (x ^ "aa")
and f x = x;;

where f is not generalized. But you can write:
let rec f x = x;;
let rec a x = f (x + 1)
and b x = f (x ^ "aa");;

--
Daniel de RAUGLAUDRE
daniel.de_rauglaudre@inria.fr
http://cristal.inria.fr/~ddr/

@vicuna
Copy link
Author

vicuna commented Apr 30, 2000

Comment author: administrator

Hi Manuel,

type a = int collection
and b = string collection
and 'a collection = 'a list;;
yields:
This type string should be an instance of type int
where "this type" refers to the "string" argument in 'b' definition.
Look like the compiler does not treat collection as a properly parameterized
type.

Actually, it treats parameterized types like polymorphic functions:
those are monomorphic inside the recursive definition, and polymorphic
outside. For types, this means that a parameterized type 'a t
must be used only as 'a t inside the type...and... declaration.

The reason for this restriction is to prevent the creation of
non-regular type abbreviations, as in

    type 'a t = 'a list t

which can "bomb" later during typechecking. This was a bug in early
versions of OCaml 2. It has the unforturnate consequence of rejecting
definitions such as yours, though. In a way, we were too permissive
before, and now maybe err a little too much on the safe side.

  • Xavier

@vicuna
Copy link
Author

vicuna commented May 1, 2000

Comment author: administrator

There seems to be some confusion here.
This problem is well known and has been already discussed extensively on
the Caml list.
Also your statement that this worked in 2.02 surprises me a lot.
See for instance http://pauillac.inria.fr/caml/caml-list/1559.html, and the
follow-ups.
I just checked for 2.04.

    Objective Caml version 2.04

type a = int collection

and b = string collection
^^^^^^
and 'a collection = 'a list;;
This type string should be an instance of type int

To sum up what has been said before, this is not a bug, but a somehow strange
specification. That is, to support the object system, constrained types have
been introduced. And a choice has been made to infer these constraints, by
generalizing type abbreviations only after type checking the whole group
of recursive type definitions.

type a = int collection

and 'a collection = 'a list;;
type a = int list
type 'a collection = a constraint 'a = int

My personal feeling is that this specification is wrong. In particular it is
incompatible with the behaviour before the introduction of constraints, and is
only useful for objects (and maybe variants).
Another problem into some people bumped is that you may write a .mli without
the constraint, and it will be added when you compile it. Since most people
believe .mli provide all the type information, this can be very disturbing.

Another possible specification would be to require writing type constraints on
every constrained type abbreviation, rather than infer them.
I believe this is a better specification. However,

  • it will break some existing code, since one will have to write more
    information in types.
  • one has to check that recursive definitions are coherent (all constraints
    are correctly propagated). I believe that one more pass after type
    introduction
    will be enough, but this may prove rather complex.
  • as any potentially complex code in a touchy place, it has to be thoroughly
    checked.

For these reasons, this was not done for 3.00.
I hope this will be in 3.01.

Jacques Garrigue

@vicuna
Copy link
Author

vicuna commented May 1, 2000

Comment author: administrator

Thanks for your explanations. I wasn't aware of the previous discussion of
this issue. Having
failed to upgrade to 2.04, I was surprised to get the error when I upgraded
to 3.00.

-Manuel

-----Original Message-----
From: Jacques Garrigue [mailto:caml-bugs@pauillac.inria.fr]
Sent: Sunday, April 30, 2000 6:12 PM
To: Manuel Fahndrich
Subject: Re: parameterized recursive types broken (#2433)

There seems to be some confusion here.
This problem is well known and has been already discussed extensively on
the Caml list.
Also your statement that this worked in 2.02 surprises me a lot.
See for instance http://pauillac.inria.fr/caml/caml-list/1559.html, and the
follow-ups.
I just checked for 2.04.

    Objective Caml version 2.04

type a = int collection

and b = string collection
^^^^^^
and 'a collection = 'a list;;
This type string should be an instance of type int

To sum up what has been said before, this is not a bug, but a somehow
strange
specification. That is, to support the object system, constrained types have
been introduced. And a choice has been made to infer these constraints, by
generalizing type abbreviations only after type checking the whole group
of recursive type definitions.

type a = int collection

and 'a collection = 'a list;;
type a = int list
type 'a collection = a constraint 'a = int

My personal feeling is that this specification is wrong. In particular it is
incompatible with the behaviour before the introduction of constraints, and
is
only useful for objects (and maybe variants).
Another problem into some people bumped is that you may write a .mli without
the constraint, and it will be added when you compile it. Since most people
believe .mli provide all the type information, this can be very disturbing.

Another possible specification would be to require writing type constraints
on
every constrained type abbreviation, rather than infer them.
I believe this is a better specification. However,

  • it will break some existing code, since one will have to write more
    information in types.
  • one has to check that recursive definitions are coherent (all constraints
    are correctly propagated). I believe that one more pass after type
    introduction
    will be enough, but this may prove rather complex.
  • as any potentially complex code in a touchy place, it has to be thoroughly
    checked.

For these reasons, this was not done for 3.00.
I hope this will be in 3.01.

Jacques Garrigue

@vicuna
Copy link
Author

vicuna commented Mar 5, 2001

Comment author: administrator

Not a bug, but this should be corrected. 3.01 now has expected behavior.

@vicuna vicuna closed this as completed Mar 5, 2001
@vicuna vicuna added the bug label Mar 19, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant