This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

Typing of polymorphic variants
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2009-04-16 (12:44) From: Philippe Veber Subject: Re: [Caml-list] Typing of polymorphic variants
```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 Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>
>
>> > 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
>>
>
>

```