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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by sympa.inria.fr (Postfix) with ESMTPS id C8B197ED34 for ; Sun, 15 Jul 2012 18:55:51 +0200 (CEST) Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of darioteixeira@yahoo.com) identity=pra; client-ip=98.139.91.79; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="darioteixeira@yahoo.com"; x-sender="darioteixeira@yahoo.com"; x-conformance=sidf_compatible Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of darioteixeira@yahoo.com) identity=mailfrom; client-ip=98.139.91.79; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="darioteixeira@yahoo.com"; x-sender="darioteixeira@yahoo.com"; x-conformance=sidf_compatible Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@nm9.bullet.mail.sp2.yahoo.com) identity=helo; client-ip=98.139.91.79; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="darioteixeira@yahoo.com"; x-sender="postmaster@nm9.bullet.mail.sp2.yahoo.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnUEAEP1AlBii1tPeGdsb2JhbAA4DacfkTQBDAkSFQQkghsBFhwEFQECFSIBFHoBDgEGGIVcgisJAQECDASZdIZOiEIJgmiDbAEjAwEjA4lRAQYKAQGRNgOIS4x3hU8tTYhag1s X-IronPort-AV: E=Sophos;i="4.77,588,1336341600"; d="scan'208";a="166923792" Received: from nm9.bullet.mail.sp2.yahoo.com ([98.139.91.79]) by mail1-smtp-roc.national.inria.fr with SMTP; 15 Jul 2012 18:55:50 +0200 Received: from [72.30.22.79] by nm9.bullet.mail.sp2.yahoo.com with NNFMP; 15 Jul 2012 16:55:49 -0000 Received: from [98.139.91.6] by tm13.bullet.mail.sp2.yahoo.com with NNFMP; 15 Jul 2012 16:54:49 -0000 Received: from [127.0.0.1] by omp1006.mail.sp2.yahoo.com with NNFMP; 15 Jul 2012 16:54:49 -0000 X-Yahoo-Newman-Property: ymail-3 X-Yahoo-Newman-Id: 746748.74954.bm@omp1006.mail.sp2.yahoo.com Received: (qmail 9963 invoked by uid 60001); 15 Jul 2012 16:54:49 -0000 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=yahoo.com; s=s1024; t=1342371289; bh=oqwZodkAm7cwcBtxzC1rXZ6/bjdkyfnJdf7/zc3jXak=; h=X-YMail-OSG:Received:X-Mailer:Message-ID:Date:From:Reply-To:Subject:To:MIME-Version:Content-Type:Content-Transfer-Encoding; b=gXOhNMsgQK1kDbwSdx44ibhweyQGrggw94MQc7dGpQ4pKTApwG7DvyzY4riL77IJff7oZrm0puzwsuytNmQoz1p+OdtMDcNkS7IHFei69U9Uu1/9XcKwAM2TWMYt5pZ7yEbD3zqAmDlXLi6nLOlMWS9hPoykOowDk/MZCKOGh7c= DomainKey-Signature:a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.com; h=X-YMail-OSG:Received:X-Mailer:Message-ID:Date:From:Reply-To:Subject:To:MIME-Version:Content-Type:Content-Transfer-Encoding; b=ICYOkVi71Dx+PgXlkGplggssYT+enWEeFzUwDew7b+qgRcqIzUPWOOCOAhHhJZkDcn8HGbOsA6JCPP3zgG6xAE09Rqn+Cbqyx6YD/SzyzTPBQfzjtDItDe5zQtMeYhq/YEXAf5tpVPJIcGIR8lDV0caOMGWa7B0Bstl1X4cDEhc=; X-YMail-OSG: KQKGT7EVM1n5iMoIjgsq12yKG_lCjl1FCgCvaOF.s0lY.cQ RAjbQiJ1tQa4qnUWlIQF_J97Za.PylPWqKKXByDkPt.s8ncYvdsb2PaNAeTd .x6zUH73IC4CC56BRHFYuq2QV0lHdsY6obf5RxZkl65yr_H3b_mbAEhWV9sO w3Gx2mKL1Gh96j5yiexNzbiPiukjEo3yYTwBKD_O1DWN0hrshNlawHdqXecE 8MLpHOM_RApyz59ua_A7GkkaerkyCh3njZ__LFNwC1.VxhWG.oNEzOO8qTcy b2c0Mq040bLdfyhF8DGpk9AL5nZa5chop9wYtygZ0ByoyLhDpUKkyBnW7YUZ 0qRsE8Qhs42hksBaN46UKlM26CDTy.VRdekftZ4GEPKNVGgeIZVzQloKWLeo NtdUPm8sVdPn9ylQMdSJiXz3_hUkZP3DYa.k_IN3t_XLoBEhv9BuWN1AbMEf A_0Swh_U. Received: from [195.23.39.96] by web111511.mail.gq1.yahoo.com via HTTP; Sun, 15 Jul 2012 09:54:49 PDT X-Mailer: YahooMailWebService/0.8.120.356233 Message-ID: <1342371289.7422.YahooMailNeo@web111511.mail.gq1.yahoo.com> Date: Sun, 15 Jul 2012 09:54:49 -0700 (PDT) From: Dario Teixeira Reply-To: Dario Teixeira To: "caml-list@inria.fr" MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable Subject: [Caml-list] GADTs and parsers Hi, I'm revisiting an old problem with 4.00's newfangled GADTs.=A0 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.=A0 Moreover, you want to enforce the invariant that a "linkish" node (Link and Mref) may not be the ancestor of another linkish node.=A0 One possible implementa= tion: type _ inline_t =3D =A0=A0=A0 | Text: string -> [> `Nonlink ] inline_t =A0=A0=A0 | Bold: 'a inline_t list -> 'a inline_t =A0=A0=A0 | Link: string -> [> `Link ] inline_t =A0=A0=A0 | 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 =3D =A0=A0=A0 let rec process: type a. a inline_t -> a inline_t =3D function =A0=A0=A0=A0=A0=A0=A0 | Text txt=A0=A0=A0=A0=A0=A0 -> Text (String.uppercas= e txt) =A0=A0=A0=A0=A0=A0=A0 | Bold xs=A0=A0=A0=A0=A0=A0=A0 -> Bold (List.map proc= ess xs) =A0=A0=A0=A0=A0=A0=A0 | Link lnk=A0=A0=A0=A0=A0=A0 -> Link lnk =A0=A0=A0=A0=A0=A0=A0 | Mref (lnk, xs) -> Mref (lnk, List.map process xs) =A0=A0=A0 in List.map process seq But suppose now that I got from a parser a ast_t value with an almost ident= ical structure to inline_t, with the exception that it does not intrinsically satisfy the latter's invariant:=A0 (Note: for this toy example it may well = be easy to design the parser grammar such that the invariant is always preserv= ed; but suppose you're dealing with a "dumb" parser) type ast_t =3D =A0=A0=A0 | Ast_Text of string =A0=A0=A0 | Ast_Bold of ast_t list =A0=A0=A0 | Ast_Link of string =A0=A0=A0 | Ast_Mref of string * ast_t list Below is one possible implementation of a function that converts the possib= ly "broken" ast_t into an inline_t.=A0 Note how the processing is split into t= wo 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 =3D =A0=A0=A0 let rec process_nonlink =3D function =A0=A0=A0=A0=A0=A0=A0 | Ast_Text txt=A0 -> Text txt =A0=A0=A0=A0=A0=A0=A0 | Ast_Bold xs=A0=A0 -> Bold (List.map process_nonlink= xs) =A0=A0=A0=A0=A0=A0=A0 | _=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 -> assert fal= se in =A0=A0=A0 let rec process_any =3D function =A0=A0=A0=A0=A0=A0=A0 | Ast_Text txt=A0=A0=A0=A0=A0=A0 -> Text txt =A0=A0=A0=A0=A0=A0=A0 | Ast_Bold xs=A0=A0=A0=A0=A0=A0=A0 -> Bold (List.map = process_any xs) =A0=A0=A0=A0=A0=A0=A0 | Ast_Link lnk=A0=A0=A0=A0=A0=A0 -> Link lnk =A0=A0=A0=A0=A0=A0=A0 | Ast_Mref (lnk, xs) -> Mref (lnk, List.map process_n= onlink xs) =A0=A0=A0 in List.map process_any seq Now here's my problem: suppose I wanted to avoid the branch duplication present in the above function.=A0 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.=A0 Moreove= r, it is not enough to simply add the type annotations for subfunction 'proces= s', as was done in 'uppercase'. let inlineseq_from_astseq seq =3D =A0=A0=A0 let rec process allow_link ast =3D match (allow_link, ast) with =A0=A0=A0=A0=A0=A0=A0 | (_, Ast_Text txt)=A0=A0=A0=A0=A0=A0=A0=A0=A0 -> Tex= t txt =A0=A0=A0=A0=A0=A0=A0 | (x, Ast_Bold xs)=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 -> B= old (List.map (process x) xs) =A0=A0=A0=A0=A0=A0=A0 | (true, Ast_Link lnk)=A0=A0=A0=A0=A0=A0 -> Link lnk =A0=A0=A0=A0=A0=A0=A0 | (false, Ast_Link _)=A0=A0=A0=A0=A0=A0=A0 -> assert = false =A0=A0=A0=A0=A0=A0=A0 | (true, Ast_Mref (lnk, xs)) -> Mref (lnk, List.map (= process false) xs) =A0=A0=A0=A0=A0=A0=A0 | (false, Ast_Mref _)=A0=A0=A0=A0=A0=A0=A0 -> assert = false =A0=A0=A0 in List.map (process true) seq Can the single function approach be made to work?=A0 I'm having trouble fig= uring out just exactly what sort of help the compiler may require to see the code above as correct...=A0 (Assuming it is correct, of course...) Thanks in advance for your time! Cheers, Dario Teixeira