Recursive Variant problem..

Charles Bouillaguet
 Stephane Glondu
 Jacques Garrigue
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20060515 (11:24) 
From:  Jacques Garrigue <garrigue@m...> 
Subject:  Re: [Camllist] Recursive Variant problem.. 
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