From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.7 required=5.0 tests=AWL,DNS_FROM_RFC_ABUSE, DNS_FROM_RFC_POST,DNS_FROM_RFC_WHOIS autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id D883ABB84 for ; Sat, 19 Jul 2008 10:43:05 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhcBAHtFgUjOvjGvgGdsb2JhbACSPgEBCwUCBAkRA5td X-IronPort-AV: E=Sophos;i="4.31,214,1215381600"; d="scan'208";a="13267506" Received: from web54605.mail.re2.yahoo.com ([206.190.49.175]) by mail2-smtp-roc.national.inria.fr with SMTP; 19 Jul 2008 10:43:05 +0200 Received: (qmail 64359 invoked by uid 60001); 19 Jul 2008 08:43:04 -0000 DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.com; h=Received:X-Mailer:Date:From:Subject:To:Cc:In-Reply-To:MIME-Version:Content-Type:Content-Transfer-Encoding:Message-ID; b=vGQ8YBNW7ItM9TzM+oFnnxrWVUhdTWIHJ+BsPh3QzI/9wEDDS5PwFgUGJmdyRXpff9K+h2XvfCutYAjVppjdDVafY2zqOX5OS3BhQm+bSOc3ZtPWeAEy2J1m7ZMxkGbSMkiSDTE/C6fn+RgRWXW6gK3ppOcwLwz82qXUy0JOa7g=; Received: from [212.13.62.126] by web54605.mail.re2.yahoo.com via HTTP; Sat, 19 Jul 2008 01:43:04 PDT X-Mailer: YahooMailWebService/0.7.218 Date: Sat, 19 Jul 2008 01:43:04 -0700 (PDT) From: Dario Teixeira Subject: Re: [Caml-list] Troublesome nodes To: Jacques Garrigue Cc: caml-list@yquem.inria.fr In-Reply-To: <20080719.112314.52190643.garrigue@math.nagoya-u.ac.jp> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Message-ID: <271056.64261.qm@web54605.mail.re2.yahoo.com> X-Spam: no; 0.00; nodes:01 abbrevs:01 node:01 sig:01 node:01 val:01 val:01 struct:01 seq:01 seq:01 summarize:01 invariants:01 ocaml:01 nodes:01 superset:01 Hi, > I don't understand your counter-example. In typechecks without any > problem, even in older versions. May you did cut it down too much? Perhaps... ;-) Here is the full code, producing an error in version "3.11+dev12 Private_abbrevs+natdynlink (2008-02-29)", compiled via GODI: module rec Node: sig type nonlink_node_t =3D [ `Text of string | `Bold of Node.super_node_t = list ] type link_node_t =3D [ `See of string | `Mref of string * nonlink_node_= t list ] type super_node_t =3D [ nonlink_node_t | link_node_t ] type (+'a, 'b) t =3D private 'a constraint 'a =3D [< super_node_t ] val text: string -> ([> nonlink_node_t], [> `Basic]) t val bold: ([< super_node_t], 'a) t list -> ([> nonlink_node_t], 'a) t val see: string -> ([> link_node_t], [> `Basic]) t val mref: string -> (nonlink_node_t, 'a) t list -> ([> link_node_t], [>= `Complex]) t val make_basic: ('a, [< `Basic]) t list -> ('a, [`Basic]) t list val make_complex: ('a, [< `Basic | `Complex]) t list -> ('a, [`Complex]= ) t list end =3D struct type nonlink_node_t =3D [ `Text of string | `Bold of Node.super_node_t = list ] type link_node_t =3D [ `See of string | `Mref of string * nonlink_node_= t list ] type super_node_t =3D [ nonlink_node_t | link_node_t ] type (+'a, 'b) t =3D 'a constraint 'a =3D [< super_node_t ] let text txt =3D `Text txt let bold seq =3D `Bold (seq :> (super_node_t, 'a) t list) let see ref =3D `See ref let mref ref seq =3D `Mref (ref, seq) let make_basic n =3D n let make_complex n =3D n end > By the way, I somehow get the feeling that your solution is > over-engineered. You shouldn't need all that many constraints. > I you could find a way to use private rows rather than private > abbreviations, your code might be much simpler. > But I'm sorry I couldn't follow the whole discussion on your problem. > I you could summarize it shortly, with the basic code (without phantom > types) and the invariants you are trying to enforce, I might try to > look into it. Thanks Jacques, I would really appreciate it. I'm stuck at this point, so any help is welcome. Moreover, this is in fact a neat problem, so any Ocam= l hacker should be able to enjoy it. Here follows a complete description of the problem, unprejudiced by the current solution. I have two types of documents, "basic" and "complex". Both are composed of a list of nodes. The difference between them is that complex documents may use a superset of the kinds of nodes available for basic documents. Namely, while basic documents may only use "Text", "Bold", and "See" nodes, complex documents may also use "Mref" nodes in addition to those three. In total, there are therefore only four different kinds of nodes. Two of those, "Text" and "See" are terminal nodes; the other two, "Bold" and "Mref= " are defined via recursion. There is one additional restriction: "See" and "Mref" produce links, and links may not be the immediate ancestors of other links (note that since "See" is a terminal node and cannot therefore be a parent, in practice this rule is identical to saying that "Mref" may not the parent of "See"). Disregarding the basic/complex distinction, nodes could be defined as follo= ws: type super_node_t =3D | Nonlink_node of nonlink_node_t | Link_node of link_node_t and nonlink_node_t =3D | Text of string | Bold of super_node_t list and link_node_t =3D | Mref of string * nonlink_node_t list | See of string The table below summarises the properties of each node: Node:=09Allowed for:=09Definition:=09Produces link? ------------------------------------------------------ Text=09basic/complex=09terminal=09no Bold=09basic/complex=09rec=09=09no See=09basic/complex=09terminal=09yes Mref=09complex=09=09rec=09=09yes There is one final, important, requirement. I want to be able to pattern-match on nodes from the outside of the module. To build a Node-to-Node function, for example. To conclude, I'll leave you with some sample documents. Some are valid, but others are not. The compiler should catch the latter. (* valid *) let doc1 =3D make_basic =09=09[ =09=09text "foo"; =09=09bold [text "bar"]; =09=09see "ref" =09=09] (* valid *) let doc2 =3D make_complex =09=09[ =09=09text "foo"; =09=09bold [text "bar"]; =09=09see "ref" =09=09] (* valid *) let doc3 =3D make_complex =09=09[ =09=09text "foo"; =09=09mref "ref" [text "bar"] =09=09] (* Invalid because a link node is the parent of another *) let doc4 =3D make_complex =09=09[ =09=09mref "ref" [see "foo"] =09=09] (* Invalid because basic documents do not allow Mref nodes *) let doc5 =3D make_basic =09=09[ =09=09text "foo"; =09=09mref "ref" [text "bar"] =09=09] Best regards, Dario Teixeira =0A=0A=0A __________________________________________________________= =0ANot happy with your email address?.=0AGet the one you really want - mill= ions of new email addresses available now at Yahoo! http://uk.docs.yahoo.co= m/ymail/new.html