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 0F3617FCCB for ; Mon, 27 Apr 2015 14:17:57 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of jpathy@fssrv.net) identity=pra; client-ip=209.85.212.169; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jpathy@fssrv.net"; x-sender="jpathy@fssrv.net"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of jpathy@fssrv.net designates 209.85.212.169 as permitted sender) identity=mailfrom; client-ip=209.85.212.169; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jpathy@fssrv.net"; x-sender="jpathy@fssrv.net"; 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-wi0-f169.google.com) identity=helo; client-ip=209.85.212.169; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jpathy@fssrv.net"; x-sender="postmaster@mail-wi0-f169.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0AyAgCnJz5VlKnUVdFcDoNRXAWDFcR3hgwCgSkHOxEBAQEBAQEBEQEBAQEHCwsJHzCEIQEBBBIRBBkBATcBDwsLDQICJgICIhIBBQEcBhMiiAmlbT4xiklwhGEBBY5xAQEBAQYBAQEBARcGCoEXiheFBQeCaIFFi2KQMZQXEiOBFYNaXR4xAYJDAQEB X-IPAS-Result: A0AyAgCnJz5VlKnUVdFcDoNRXAWDFcR3hgwCgSkHOxEBAQEBAQEBEQEBAQEHCwsJHzCEIQEBBBIRBBkBATcBDwsLDQICJgICIhIBBQEcBhMiiAmlbT4xiklwhGEBBY5xAQEBAQYBAQEBARcGCoEXiheFBQeCaIFFi2KQMZQXEiOBFYNaXR4xAYJDAQEB X-IronPort-AV: E=Sophos;i="5.11,656,1422918000"; d="scan'208";a="137758905" Received: from mail-wi0-f169.google.com ([209.85.212.169]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 27 Apr 2015 14:17:56 +0200 Received: by widdi4 with SMTP id di4so87508046wid.0 for ; Mon, 27 Apr 2015 05:17:56 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=fssrv.net; s=google; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=BoPostqIFRCKSIFVytBztkOdoS9jVT9Ai/FmaSemkkw=; b=VlOk5y9JtVlXdE9SxbqTf5csA2ggRUFV+xZIxs8ylp7BOQf/6ZK+YkPeZpKWw9xham cVCJdTrZisnF1ZNmjClzlKGDYtn6yzWi4aJ0Lyxp5a8NhrlfptTXKjzlFElpCwLYuA0f FXCgZ48e2rs3MSrsjLjREh6jGBCLO8m4teeOU= X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:date :message-id:subject:from:to:cc:content-type; bh=BoPostqIFRCKSIFVytBztkOdoS9jVT9Ai/FmaSemkkw=; b=Lq6hCU8ztHqEWy0dyeB1zIGNSswuKEzBtPKcWfwOAqYEy3us91SiyoRjwioa6SBstM s82xgF+wnWlZljgkrgQyQQ8mJ/J6QIbZA3HpHC1AcDtY7palIYEQ9R/js6nY527aRyat DJNoXpaueVl6i0nfIRr7khbZzCIbWPs/zuY6WeS7TDueiaN+ryH0IcGRd4dHt40h7sUJ Hzy2kxDpCHtKU5u6VPcT3lHIKe/C8BzR359Twmy9VP+oN/5xCqnQojLtMWNklixn36iF 6kKXCKs3Z9+lr752ZsNm1t2e+diUFDlo8LznorSEKfSV4+HwJhJ067DaPg4ddTS21Gm+ AQxg== X-Gm-Message-State: ALoCoQnK4NdUSgt8NAlsX5Y6SmGIjJ1oc0yuZEq0iMmP2W81Ok1VtsQdHcpLhAHUyhyl9O2u6SDd MIME-Version: 1.0 X-Received: by 10.180.74.208 with SMTP id w16mr20114114wiv.31.1430137076554; Mon, 27 Apr 2015 05:17:56 -0700 (PDT) Received: by 10.27.97.66 with HTTP; Mon, 27 Apr 2015 05:17:56 -0700 (PDT) In-Reply-To: References: Date: Mon, 27 Apr 2015 05:17:56 -0700 Message-ID: From: Jiten Pathy To: Stephen Dolan Cc: Jeremy Yallop , "caml-list@inria.fr" Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] phantom type It seems this encoding using first-class modules has overheads in the interpreter(due to the functor), whereas the gadt implementation would have no overheads. On Mon, Apr 27, 2015 at 4:51 AM, Stephen Dolan wrote: > To expand a little on Jeremy's answer, you can encode the expr type as > a module signature, and then pass terms around as first-class modules. > > First, you make a module signature that describes the ways of > constructing a term: > > module type Ctors = sig > type 'a term > val zero : int term > val succ : int term -> int term > val iszero : int term -> bool term > end > > Next, a Term is something which can construct a term using any set of Ctors: > > module type Term = sig > type a > module Build : functor (C : Ctors) -> sig > val x : a C.term > end > end > > You can make a normal datatype from this using first-class modules: > > type 'a term = (module Term with type a = 'a) > > We're jumping between the module and the core language, so the > wrapping and unwrapping makes things a bit verbose. Here's the > value-level "succ" operation, the other two are similar: > > let succ ((module T) : int term) : int term = > (module struct > type a = int > module Build = functor (C : Ctors) -> struct > module TC = T.Build (C) > let x = C.succ TC.x > end > end) > > Evaluation is one particular implementation of the term constructors, > which implements the type 'a term as just 'a: > > module Eval = struct > type 'a term = 'a > let zero = 0 > let succ n = n + 1 > let iszero n = (n = 0) > end > > Finally, you can use this evaluation module to interpret any term: > > let eval (type a) ((module T) : a term) : a = > let module M = T.Build (Eval) in M.x > > Stephen