Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000095OCamlOCaml generalpublic2000-04-28 20:392001-03-05 17:32
Reporteradministrator 
Assigned To 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0000095: parameterized recursive types broken
DescriptionFull_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


TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000364)
administrator (administrator)
2000-04-28 12:31

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 (PR#95)


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/ [^]

(0000365)
administrator (administrator)
2000-04-28 21:06

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/ [^]

(0000366)
administrator (administrator)
2000-04-30 12:39

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

(0000367)
administrator (administrator)
2000-05-01 03:11

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
(0000368)
administrator (administrator)
2000-05-01 08:41

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 (PR#95)


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

(0000369)
administrator (administrator)
2001-03-05 17:32

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

- Issue History
Date Modified Username Field Change
2005-11-18 10:13 administrator New Issue


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker