Re: [Caml-list] Typing of polymorphic variants

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

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