From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 2198FBB84 for ; Mon, 15 May 2006 13:24:17 +0200 (CEST) Received: from kurims.kurims.kyoto-u.ac.jp (kurims.kurims.kyoto-u.ac.jp [130.54.16.1]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id k4FBOFKA021715 for ; Mon, 15 May 2006 13:24:16 +0200 Received: from localhost (suiren [130.54.16.25]) by kurims.kurims.kyoto-u.ac.jp (8.13.6/8.13.6) with ESMTP id k4FBNx0V019021; Mon, 15 May 2006 20:23:59 +0900 (JST) Date: Mon, 15 May 2006 20:23:55 +0900 (JST) Message-Id: <20060515.202355.105436069.garrigue@math.nagoya-u.ac.jp> To: Charles.Bouillaguet@crans.org Cc: caml-list@yquem.inria.fr, romain.bardou@wanadoo.fr Subject: Re: [Caml-list] Recursive Variant problem.. From: Jacques Garrigue In-Reply-To: References: X-Mailer: Mew version 4.2 on Emacs 21.3 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 446864DF.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; recursive:01 arrays:01 arrays:01 variants:01 recursive:01 defines:01 occurences:01 variants:01 unification:01 decidable:01 haskell:01 ocaml:01 simulate:01 encodings:01 existential:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.4 required=5.0 tests=DNS_FROM_RFC_ABUSE autolearn=disabled version=3.0.3 From: Charles Bouillaguet > 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