Typing of polymorphic variants

Typing of polymorphic variants

[Philippe Veber]

[-- Attachment #1: Type: text/plain, Size: 340 bytes --]

Hi list,

I don't understand the following behaviour:

        Objective Caml version 3.11.0

# type t = [`A | `B of int u] and 'a u = 'a * t;;
Error: In the definition of t, type int u should be 'a u
# type t = A | B of int u and 'a u = 'a * t;;
type t = A | B of int u
and 'a u = 'a * t

Anyone's got a simple explanation for this ?

ph.

[-- Attachment #2: Type: text/html, Size: 434 bytes --]

Re: [Caml-list] Typing of polymorphic variants

[Jacques Garrigue]

From: Philippe Veber <philippe.veber@googlemail.com>
> I don't understand the following behaviour:
> 
>         Objective Caml version 3.11.0
> 
> # type t = [`A | `B of int u] and 'a u = 'a * t;;
> Error: In the definition of t, type int u should be 'a u
> # type t = A | B of int u and 'a u = 'a * t;;
> type t = A | B of int u
> and 'a u = 'a * t
> 
> Anyone's got a simple explanation for this ?

This is due to the difference between type abbreviations and
datatypes. In your first example, you are defining two types
abbreviations, and you are not allowed to instantiate a type you are
defining in mutual recursion. In the second example, you are defining a
datatype and a type abbreviation, and it is ok to instantiate the type
abbreviation inside the datatype definition.

The technical reason for this difference is the restriction to regular
types in type abbreviations. It only applies when the definitions are
mutually recursive, and do not go through any datatype definition.

Jacques Garrigue

Re: [Caml-list] Typing of polymorphic variants

[Philippe Veber]

[-- Attachment #1: Type: text/plain, Size: 1349 bytes --]

2009/4/16 Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>

> From: Philippe Veber <philippe.veber@googlemail.com>
> > I don't understand the following behaviour:
> >
> >         Objective Caml version 3.11.0
> >
> > # type t = [`A | `B of int u] and 'a u = 'a * t;;
> > Error: In the definition of t, type int u should be 'a u
> > # type t = A | B of int u and 'a u = 'a * t;;
> > type t = A | B of int u
> > and 'a u = 'a * t
> >
> > Anyone's got a simple explanation for this ?
>
> This is due to the difference between type abbreviations and
> datatypes. In your first example, you are defining two types
> abbreviations, and you are not allowed to instantiate a type you are
> defining in mutual recursion. In the second example, you are defining a
> datatype and a type abbreviation, and it is ok to instantiate the type
> abbreviation inside the datatype definition.
>
> The technical reason for this difference is the restriction to regular
> types in type abbreviations. It only applies when the definitions are
> mutually recursive, and do not go through any datatype definition.


Indeed, I noticed in other attempts that some definitions that would be
accepted in the form type t = ... type u = ... were rejected in the form
type t = ... and u = ... Now with your explanation it's clear why. Many
thanks !

ph.


>
>
> Jacques Garrigue
>

[-- Attachment #2: Type: text/html, Size: 2079 bytes --]

Re: [Caml-list] Typing of polymorphic variants

[Philippe Veber]

[-- Attachment #1: Type: text/plain, Size: 1679 bytes --]

Just for the record, one possible workaround is the following :

type ('a, 'b) gen_u = 'a * 'b
type t = [`A | `B of (int,t) gen_u]
type 'a u = 'a * t

which avoids recursive definitions between type abbreviations.

ph.



2009/4/16 Philippe Veber <philippe.veber@googlemail.com>

>
> 2009/4/16 Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
>
> From: Philippe Veber <philippe.veber@googlemail.com>
>> > I don't understand the following behaviour:
>> >
>> >         Objective Caml version 3.11.0
>> >
>> > # type t = [`A | `B of int u] and 'a u = 'a * t;;
>> > Error: In the definition of t, type int u should be 'a u
>> > # type t = A | B of int u and 'a u = 'a * t;;
>> > type t = A | B of int u
>> > and 'a u = 'a * t
>> >
>> > Anyone's got a simple explanation for this ?
>>
>> This is due to the difference between type abbreviations and
>> datatypes. In your first example, you are defining two types
>> abbreviations, and you are not allowed to instantiate a type you are
>> defining in mutual recursion. In the second example, you are defining a
>> datatype and a type abbreviation, and it is ok to instantiate the type
>> abbreviation inside the datatype definition.
>>
>> The technical reason for this difference is the restriction to regular
>> types in type abbreviations. It only applies when the definitions are
>> mutually recursive, and do not go through any datatype definition.
>
>
> Indeed, I noticed in other attempts that some definitions that would be
> accepted in the form type t = ... type u = ... were rejected in the form
> type t = ... and u = ... Now with your explanation it's clear why. Many
> thanks !
>
> ph.
>
>
>>
>>
>> Jacques Garrigue
>>
>
>

[-- Attachment #2: Type: text/html, Size: 2742 bytes --]