Recursive Variant problem..

Recursive Variant problem..

[Charles Bouillaguet]

Hello Caml-List,

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 ?
b) Is it possible to wrote that with Recursive modules, and how ?

I'm CC-ing my classmate Romain (Hi, Romain !), as he may be  
interested...

Charles Bouillaguet
-=-=-=-=-
Ens de Cachan, Currently visiting MIT.

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

[Stephane Glondu]

Charles Bouillaguet wrote:
> 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
> [...]
> a) is it possible to write that with polymorphic variants, and how ?
> b) Is it possible to wrote that with Recursive modules, and how ?

It reminds me of the following:

------------------------------------------------------------------------
** Norman Ramsey asked and Jacques Garrigue answered:

  > I'm trying to write a small, extensible interpreter, and I'd like to
  > use polymorphic variants as the extension mechanism.  But I'm getting
  > stuck on very simple things.  For example, I would like the value
type
  > to include a few simple values, but I would also like it to be
  > extensible, thus:
  >
  >   type value = [ `Nil
  >                | `Number   of float
  >                | `String   of string
  >                | `Function of [>value] list -> [>value]
  >                | `Table    of ([>value], [>value]) Hashtbl.t
  >                ]
  >
  > However, when I do this, the compiler complains that
  >
  >   The type constructor value is not yet completely defined
  >
  > Is there some way to define a recursive, *extensible* type using
  > polymorphic variants?

Have a look at "Private rows: abstracting the unnamed" and
"Code reuse through polymorphic variants" at
<http://www.math.nagoya-u.ac.jp/~garrigue/papers/>

They both give examples of how to define extensible languages using
polymorphic variants. The first one relies on an experimental feature
only available in the CVS version of ocaml.

========================================================================

I haven't read the papers yet, so I cannot go further.

> I'm CC-ing my classmate Romain (Hi, Romain !), as he may be interested...

And what about me? :-(

-- 
Stephane Glondu
ENS de Cachan, currently visiting Keio Universty (Tokyo)

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

[Jacques Garrigue]

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

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

[Jacques Garrigue]

> From: Charles Bouillaguet <Charles.Bouillaguet@crans.org>
> > 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

> The trouble is that the array case takes 'sort as a parameter, meaning
> that we would need an infinity of such duplicates.
> 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.)

Note that this can be solved by introducing a nominal type (record or
sum type) that breaks the irregular cycles. Here the following is
sufficient.

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: 'sort; desc:
     [ `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

Probably this is not you wanted, but just to make things clear.

Jacques Garrigue