Re: [Caml-list] Typing of polymorphic variants

[Philippe Veber <philippe.veber@googlemail.com>]

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