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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 3419B7EE7D for ; Thu, 21 May 2015 20:44:19 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of rlepigre@gmail.com) identity=pra; client-ip=74.125.82.53; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rlepigre@gmail.com"; x-sender="rlepigre@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of rlepigre@gmail.com designates 74.125.82.53 as permitted sender) identity=mailfrom; client-ip=74.125.82.53; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rlepigre@gmail.com"; x-sender="rlepigre@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wg0-f53.google.com) identity=helo; client-ip=74.125.82.53; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rlepigre@gmail.com"; x-sender="postmaster@mail-wg0-f53.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0A0AQDGJl5VmzVSfUpcFoJQfl6DH798gVmFd4FMOhIBAQEBAQEBEQEBAQEBBgsLCSEuhCMBAQMBEhEECwENATgBAwELAQUFGgIFIQICDwUgAQUBIjWHdQMKCAEECKISPjGLPoRkmggnDYUYAQUOgROKGYRSgyIvgRYFly2GU4Fnk201gRVcKGaCM20BgkYBAQE X-IPAS-Result: A0A0AQDGJl5VmzVSfUpcFoJQfl6DH798gVmFd4FMOhIBAQEBAQEBEQEBAQEBBgsLCSEuhCMBAQMBEhEECwENATgBAwELAQUFGgIFIQICDwUgAQUBIjWHdQMKCAEECKISPjGLPoRkmggnDYUYAQUOgROKGYRSgyIvgRYFly2GU4Fnk201gRVcKGaCM20BgkYBAQE X-IronPort-AV: E=Sophos;i="5.13,471,1427752800"; d="scan'208";a="152468018" Received: from mail-wg0-f53.google.com ([74.125.82.53]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 21 May 2015 20:44:07 +0200 Received: by wghq2 with SMTP id q2so94569474wgh.1 for ; Thu, 21 May 2015 11:44:06 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=sender:date:from:to:cc:subject:message-id:references:mime-version :content-type:content-disposition:content-transfer-encoding :in-reply-to:user-agent; bh=dLI4Bvp5SLlIGIGP8jZfkQTZes8nAbc2/HqbInbHd8s=; b=hR+lLFiq2Y5JocpL5BQlLKrcBEdBKHNDYzwLLNLzNkl3TmUxBzNQGhxfuaNHiqonts SH3Odlw+d+Yg/d665OpiVaMUAYYEi2sTsdYdgSMCqKGWyEqOZvJ2/V/OQDTgJzqXkQ2T sA2YeuyLfo7rNgJruF+r3vIlxGVImNMIWpSVvptyxqsDLYbfkt4KXkDZ74MK0vgFNlfc SC7pm8CWdINetwmfUro6Mo5xcu/Mu1RI7k14uffEBbyh6SARPU6PBxhMB412Rwgf5jeW 8AFKw4EgKjDecqGRZ6L4hSlqpTW6JHVwnnkn8FaDhXsNKqR2dvkttfAzSb3Emzleu6ny +RuQ== X-Received: by 10.180.12.104 with SMTP id x8mr107175wib.85.1432233846588; Thu, 21 May 2015 11:44:06 -0700 (PDT) Received: from localhost ([2a01:e35:399a:59e0:ae7b:a1ff:feb1:4789]) by mx.google.com with ESMTPSA id hu1sm3896688wib.6.2015.05.21.11.44.05 (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 21 May 2015 11:44:05 -0700 (PDT) Sender: Rodolphe Lepigre Date: Thu, 21 May 2015 20:44:04 +0200 From: Rodolphe Lepigre To: Trevor Smith Cc: "caml-list@inria.fr" Message-ID: <20150521184404.GA598@HPArchRod> References: MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) Subject: Re: [Caml-list] GADTs and JSON Hi, > Is it possible to encode a recursive, heterogenous map and list datastructure > with GADTs? > > I want to encode JSON (there are already a couple of great libraries out there > so this is kind of an academic question). I would like to have functions that > can only take a JSON map type, for example to take a json map and return a > value. The key here is that the map can hold values of type int,string and also > maps. Is this possible? > > eg get : (map : map json) -> key:string -> 'a json > > Thank you. > > Trevor You should probably have a look at the examples given for GADTs on the page about language extensions (advanced examples section): http://caml.inria.fr/pub/docs/manual-ocaml-400/manual021.html#toc85 Not so long ago I used equality types to encode collections of object of different types. Here is an example with lists and a function for obtaining the n-th element. ########## type (_,_) eq = Eq : ('a,'a) eq type 'a typ = | Int : int typ | Float : float typ | Pair : 'a typ * 'b typ -> ('a * 'b) typ let rec equal : type a b. a typ -> b typ -> (a,b) eq option = fun t1 t2 -> match (t1,t2) with | (Int , Int ) -> Some Eq | (Float , Float ) -> Some Eq | (Pair(a,b) , Pair(c,d)) -> begin match (equal a c, equal b d) with | (Some Eq, Some Eq) -> Some Eq | _ -> None end | _ -> None type _ tlist' = | Nil : unit tlist' | Cons : ('a typ * 'a * unit tlist') -> unit tlist' type tlist = unit tlist' let rec nth : type a. tlist -> int -> a typ -> a = fun l n ty -> match (l, n) with | (Nil , _) -> raise Not_found | (Cons(ty',t,_), 0) -> begin match equal ty ty' with | Some Eq -> t | None -> invalid_arg "Ill type in nth" end | (Cons(_,_,l) , _) -> nth l (n-1) ty let l = Cons(Int, 3, Cons(Float, 4.2, Nil)) let n : int = nth l 0 Int let f : float = nth l 1 Float ########## Regards, Rodolphe -- Rodolphe Lepigre LAMA, Université de Savoie, FRANCE http://lama.univ-savoie.fr/~lepigre/