Re: [Caml-list] Recursive Variant problem..

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

From: Charles Bouillaguet <Charles.Bouillaguet@crans.org>

> I would like to write a type which describe some kind of term in a  
> toy programming language. It has sets, but not sets of sets
> 
> type 'a array_ = [`Array of 'a]
> type base_sort = [`Int | `Float | `Object | `Array of base_sort]  (*  
> arrays of arrays are OK *)
> type sort = [base_sort | `Set of  
> base_sort]                                  (* sets of sets are NOT OK*)
> 
> The problem appear when I want to define my values :
> 
> type 'sort array_state = 'sort * [`ArrayStateVar of string |  
> `ArrayWrite of 'me  * 'sort base_value * [`Int] base_value * 'sort  
> base_value] as 'me
> and 'sort base_value = 'sort * [`Inert of unit | `FieldRead of  
> [`Object] base_value * 'sort field | `ArrayRead of 'sort array_state  
> * ('sort array_) base_value * [`Int] base_value]
> and 'sort field = 'sort * [`FieldVar of string | `FieldWrite of 'me *  
> [`Object] base_value * 'sort base_value] as 'me
> 
> is refused with error :
> =========================
> In the definition of base_value, type
> [ `Int ] array_state
> should be
> 'a array_state
> ======================
> 
> I then have two questions :
> 
> a) is it possible to write that with polymorphic variants, and how ?

There are two problems here. The first one is that mutually recursive
type abbreviations are monomorphic. As a result, if you use several
times array_state inside the same recursive type definition (that also
defines array_state), all its occurences should have the same type.

At first I thought it was the only problem. Then the solution would be
to duplicate definitions (i.e. define int_base_value,
object_base_value...)
The trouble is that the array case takes 'sort as a parameter, meaning
that we would need an infinity of such ducplicates.
Here is the second problem: by nature, polymorphic variants only allow
regular types (that can be represented by a regular graph), and your
definitions do not represent a regular type (you can get ever deeper
arrays.)

> b) Is it possible to wrote that with Recursive modules, and how ?

Recursive modules do not help, as this is a fundemental restriction of
structural types (to keep unification decidable.)

What you need here is GADTs, which are already in Haskell (GHC), and a
work in progress for ocaml.
In your case it should also be possible to simulate them by using
encodings of GADTs using existential types (available through
polymorphic record fields), but this is rather heavy weight to use. I
have some sample code to do that, but it is on a broken laptop...

Jacques