From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by sympa.inria.fr (Postfix) with ESMTPS id 8A4AD7ED34 for ; Sun, 15 Jul 2012 21:55:28 +0200 (CEST) Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lpw25@hermes.cam.ac.uk) identity=pra; client-ip=131.111.8.141; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="lpw25@hermes.cam.ac.uk"; x-sender="lpw25@hermes.cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lpw25@hermes.cam.ac.uk) identity=mailfrom; client-ip=131.111.8.141; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="lpw25@hermes.cam.ac.uk"; x-sender="lpw25@hermes.cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail4-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@ppsw-41.csi.cam.ac.uk) identity=helo; client-ip=131.111.8.141; receiver=mail4-smtp-sop.national.inria.fr; envelope-from="lpw25@hermes.cam.ac.uk"; x-sender="postmaster@ppsw-41.csi.cam.ac.uk"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AuoBAA4fA1CDbwiNmWdsb2JhbABFuDIiAQEBAQEICwsbJ4IhAQUnEUEQAQpGVwaIIASxDYkEi0CGAgObEY0Q X-IronPort-AV: E=Sophos;i="4.77,588,1336341600"; d="scan'208";a="150714441" Received: from ppsw-41.csi.cam.ac.uk ([131.111.8.141]) by mail4-smtp-sop.national.inria.fr with ESMTP; 15 Jul 2012 21:55:27 +0200 X-Cam-AntiVirus: no malware found X-Cam-SpamDetails: not scanned X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/ Received: from hermes-2.csi.cam.ac.uk ([131.111.8.54]:48844) by ppsw-41.csi.cam.ac.uk (smtp.hermes.cam.ac.uk [131.111.8.156]:25) with esmtpa (EXTERNAL:lpw25) id 1SqUuc-0000Cl-St (Exim 4.72) (return-path ); Sun, 15 Jul 2012 20:55:27 +0100 Received: from prayer by hermes-2.csi.cam.ac.uk (hermes.cam.ac.uk) with local (PRAYER:lpw25) id 1SqUuc-0005NJ-Tz (Exim 4.67) (return-path ); Sun, 15 Jul 2012 20:55:26 +0100 Received: from [86.26.0.34] by webmail.hermes.cam.ac.uk with HTTP (Prayer-1.3.5); 15 Jul 2012 20:55:26 +0100 Date: 15 Jul 2012 20:55:26 +0100 From: Leo P White To: Dario Teixeira Cc: "caml-list@inria.fr" Message-ID: In-Reply-To: <1342371289.7422.YahooMailNeo@web111511.mail.gq1.yahoo.com> References: <1342371289.7422.YahooMailNeo@web111511.mail.gq1.yahoo.com> X-Mailer: Prayer v1.3.5 Mime-Version: 1.0 Content-Type: text/plain; format=flowed; charset=ISO-8859-1 Sender: "L.P. White" Subject: Re: [Caml-list] GADTs and parsers What about something like (not really tested): type _ guard_t = | Nonlinked: [> `Nonlink ] guard_t | Either: [> `Nonlink | `Link ] guard_t let inlineseq_from_astseq seq = let rec process : type a. a guard_t -> ast_t -> a inline_t = fun guard ast -> match (guard, ast) with | (Nonlinked, Ast_Text txt) -> Text txt | (Either, Ast_Text txt) -> Text txt | (x, Ast_Bold xs) -> Bold (List.map (process x) xs) | (Either, Ast_Link lnk) -> Link lnk | (Either, Ast_Mref (lnk, xs)) -> Mref (lnk, List.map (process Nonlinked) xs) | _ -> assert false in List.map (process Either) seq Leo On Jul 15 2012, Dario Teixeira wrote: >Hi, > > I'm revisiting an old problem with 4.00's newfangled GADTs. Suppose you > have four kinds of inline nodes, two of which (Text and Link) are leaves, > while the other two (Bold and Mref) are the parents of other nodes. > Moreover, you want to enforce the invariant that a "linkish" node (Link > and Mref) may not be the ancestor of another linkish node. One possible > implementation: > >type _ inline_t = > | Text: string -> [> `Nonlink ] inline_t > | Bold: 'a inline_t list -> 'a inline_t > | Link: string -> [> `Link ] inline_t > | Mref: string * [< `Nonlink ] inline_t list -> [> `Link ] inline_t > > > Defining a simple transformation function (in this case one which > uppercases all text) is also straightforward, just as long as one > includes the proper type annotations: > >let uppercase seq = > let rec process: type a. a inline_t -> a inline_t = function > | Text txt -> Text (String.uppercase txt) > | Bold xs -> Bold (List.map process xs) > | Link lnk -> Link lnk > | Mref (lnk, xs) -> Mref (lnk, List.map process xs) > in List.map process seq > > > But suppose now that I got from a parser a ast_t value with an almost > identical structure to inline_t, with the exception that it does not > intrinsically satisfy the latter's invariant: (Note: for this toy > example it may well be easy to design the parser grammar such that the > invariant is always preserved; but suppose you're dealing with a "dumb" > parser) > >type ast_t = > | Ast_Text of string > | Ast_Bold of ast_t list > | Ast_Link of string > | Ast_Mref of string * ast_t list > > > Below is one possible implementation of a function that converts the > possibly "broken" ast_t into an inline_t. Note how the processing is > split into two separate functions -- one which deals only with nonlinks, > and other that takes anything -- so we can be sure to satisfy the GADT > constraints. > >let inlineseq_from_astseq seq = > let rec process_nonlink = function > | Ast_Text txt -> Text txt > | Ast_Bold xs -> Bold (List.map process_nonlink xs) > | _ -> assert false in > let rec process_any = function > | Ast_Text txt -> Text txt > | Ast_Bold xs -> Bold (List.map process_any xs) > | Ast_Link lnk -> Link lnk > | Ast_Mref (lnk, xs) -> Mref (lnk, List.map process_nonlink xs) > in List.map process_any seq > > > Now here's my problem: suppose I wanted to avoid the branch duplication > present in the above function. The code below seems to do the trick, > while at the same time ensuring that the result is always a valid > inline_t. However, the compiler has trouble seeing that the code is a > sound way to produce convert an ast_t into an inline_t, and rejects the > code. Moreover, it is not enough to simply add the type annotations for > subfunction 'process', as was done in 'uppercase'. > > let inlineseq_from_astseq seq = let rec process allow_link ast = > match (allow_link, ast) with | (_, Ast_Text txt) -> Text > txt | (x, Ast_Bold xs) -> Bold (List.map (process x) > xs) | (true, Ast_Link lnk) -> Link lnk | (false, > Ast_Link _) -> assert false | (true, Ast_Mref (lnk, xs)) > -> Mref (lnk, List.map (process false) xs) | (false, Ast_Mref > _) -> assert false in List.map (process true) seq > > > Can the single function approach be made to work? I'm having trouble > figuring out just exactly what sort of help the compiler may require to > see the code above as correct... (Assuming it is correct, of course...) > >Thanks in advance for your time! >Cheers, >Dario Teixeira > > >