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 concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id BB131BB84 for ; Wed, 28 Jun 2006 18:27:07 +0200 (CEST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id k5SGR74E015324 for ; Wed, 28 Jun 2006 18:27:08 +0200 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id SAA21744 for ; Wed, 28 Jun 2006 18:27:07 +0200 (MET DST) Received: from nz-out-0102.google.com (nz-out-0102.google.com [64.233.162.204]) by nez-perce.inria.fr (8.13.6/8.13.6) with ESMTP id k5SGR61a009107 for ; Wed, 28 Jun 2006 18:27:06 +0200 Received: by nz-out-0102.google.com with SMTP id n1so1881515nzf for ; Wed, 28 Jun 2006 09:27:05 -0700 (PDT) DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:to:subject:mime-version:content-type; b=CGkikBCKWv3wAUldQ2C25x16sy5hg1oow9LemknmNzWp7tjNSd+d4kfluFxMitebSNeGHlwKaFQAzwMqKF8MF97KZxEUt12FnV/kBApdjbY9kPCcO3+KEenJwXc2ngsYcocISycIYlYfsGgHTzHYr46t54hlPy2KjjLK/mtxOBg= Received: by 10.36.74.19 with SMTP id w19mr1355997nza; Wed, 28 Jun 2006 09:27:05 -0700 (PDT) Received: by 10.36.57.20 with HTTP; Wed, 28 Jun 2006 09:27:05 -0700 (PDT) Message-ID: Date: Wed, 28 Jun 2006 11:27:05 -0500 From: "Seth J. Fogarty" To: caml-list Subject: Question on Variant Types MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="----=_Part_11615_15927198.1151512025121" X-j-chkmail-Score: MSGID : 44A2ADDA.000 on nez-perce : j-chkmail score : X : 0/20 1 X-Miltered: at concorde with ID 44A2ADDB.002 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 44A2ADDA.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; foo:01 foo:01 annotations:01 statically:01 annotations:01 statically:01 W12:98 assert:01 assert:01 signatures:01 signatures:01 functions:01 functions:01 int:01 int: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.3 required=5.0 tests=HTML_10_20,HTML_MESSAGE, RCVD_BY_IP autolearn=disabled version=3.0.3 ------=_Part_11615_15927198.1151512025121 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Content-Disposition: inline I have a situation in which I have two kinds of trees. The simplified example is linked lists: type foo = [`Nil | `Tree of foo] type bar = [`Nil | `Leaf of int | `Tree of bar] I have a tree with only shape, and a tree with some information. I want to be able to distinguish between these. Here I have functions to assert types, but these annotations will be part of the signatures of functions actually doing things in the real code. But I do want to have these static checks on contests. let f x : foo = x let g x : bar = x let a = `Tree (`Nil) let b = `Tree (a) let c = `Tree (f a) let d = `Tree (`Leaf 1) As is proper, I can run f on a, b, and c, but not on d. D is not a valid foo. But I cannot run g on c. This makes sense, as I have said 'a tree of bars contains a bars.' But I want to somehow note that a tree of bars MIGHT contain foo's. Is there any way to annotate this? I cannot say type bar = [`Nil | `Leaf of int | `Tree of [bar | foo]] as bar is not fully defined. I cannot say type bar = [`Leaf of int | `Tree of bar | foo] because tree cannot have two separate types. The current, icky, non-variant type solution has the equivalent of type 'a foo = Nil | Tree of foo | F of 'a With special things filling in for 'a. But I end up putting EVERYTHING in 'a because I don't have a way to statically guaranteeing that my "leaf foo"'s are valid "leaf or branch foo's". So I have a weaker system than I want. Any suggestions? Seems like variant types should work here. I COULD add type annotations to functions, check them, and then remove the annotations so that my types are never constrained. I think that might even work. But it seems rather icky. -- Seth Fogarty sfogarty@[gmail.com|rice.edu|livejournal] Neep-neep at large AIM: Sorrath "I know there are people in this world who do not love their fellow human beings - and I hate people like that" --Tom Lehrer. ------=_Part_11615_15927198.1151512025121 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline I have a situation in which I have two kinds of trees. The simplified example is linked lists:

type foo = [`Nil | `Tree of foo]
type bar = [`Nil | `Leaf of int | `Tree of bar]

I have a tree with only shape, and a tree with some information. I want to be able to distinguish between these.  Here I have functions to assert types, but these annotations will be part of the signatures of functions actually doing things in the real code. But I do want to have these static checks on contests.

let f x : foo = x
let g x : bar = x
let a = `Tree (`Nil)
let b = `Tree (a)
let c = `Tree (f a)
let d = `Tree (`Leaf 1)

As is proper, I can run f on a, b, and c, but not on d. D is not a valid foo.
But I cannot run g on c. This makes sense, as I have said 'a tree of bars contains a bars.' But I want to somehow note that a tree of bars MIGHT contain foo's. Is there any way to annotate this?

I cannot say

type bar = [`Nil | `Leaf of int | `Tree of [bar | foo]] as bar is not fully defined.
I cannot say
type bar = [`Leaf of int | `Tree of bar | foo] because tree cannot have two separate types.

The current, icky, non-variant type solution has the equivalent of
type 'a foo = Nil | Tree of foo | F of 'a
With special things filling in for 'a. But I end up putting EVERYTHING in 'a because I don't have a way to statically guaranteeing that my "leaf foo"'s  are valid "leaf or branch foo's". So I have a weaker system than I want.

Any suggestions? Seems like variant types should work here. I COULD add type annotations to functions, check them, and then remove the annotations so that my types are never constrained. I think that might even work. But it seems rather icky.

--
Seth Fogarty             sfogarty@[gmail.com|rice.edu|livejournal]
Neep-neep at large    AIM: Sorrath
"I know there are people in this world who do not love their fellow
human beings - and I hate people like that" --Tom Lehrer. ------=_Part_11615_15927198.1151512025121--