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 7A8B07FD02 for ; Mon, 27 Apr 2015 13:51:14 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of stedolan@stedolan.net) identity=pra; client-ip=209.85.214.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="stedolan@stedolan.net"; x-sender="stedolan@stedolan.net"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of stedolan@stedolan.net) identity=mailfrom; client-ip=209.85.214.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="stedolan@stedolan.net"; x-sender="stedolan@stedolan.net"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ob0-f174.google.com) identity=helo; client-ip=209.85.214.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="stedolan@stedolan.net"; x-sender="postmaster@mail-ob0-f174.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0AWAgDEIT5Vm67WVdFcg19hgxXEd4c3BzsRAQEBAQEBAREBAQEBAQYLCwkhLoQhAQEEEhEEUhABCgsDDAImAgIiEgEFARwGGxqICaVePjGLOY5ahScKgReKF4d0L4EWAQScDpQXEiOBFYQYgjKBAAEBAQ X-IPAS-Result: A0AWAgDEIT5Vm67WVdFcg19hgxXEd4c3BzsRAQEBAQEBAREBAQEBAQYLCwkhLoQhAQEEEhEEUhABCgsDDAImAgIiEgEFARwGGxqICaVePjGLOY5ahScKgReKF4d0L4EWAQScDpQXEiOBFYQYgjKBAAEBAQ X-IronPort-AV: E=Sophos;i="5.11,656,1422918000"; d="scan'208";a="137753029" Received: from mail-ob0-f174.google.com ([209.85.214.174]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 27 Apr 2015 13:51:13 +0200 Received: by obfe9 with SMTP id e9so80981425obf.1 for ; Mon, 27 Apr 2015 04:51:11 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:sender:in-reply-to:references:date :message-id:subject:from:to:cc:content-type; bh=C8gy1XdAwht0Mhe9vgBrLy3GseIT3Jrxi+7g5RrUT/k=; b=TMGdr6sXC6xPwE11AReG943BkiR/QBR39EfKE1JL/L3k751X/0tPn0o8iccST+wNdy oySSHPbILZa4mKIFgohsp8nwOyLhTtiIH4t4QRxBE11JB+468VevM2kKTUFsEgEtHCVd pIcaFM/mwDCNFkieInIGiwjGBLrONsb4L00/PEgh4FS/S/8tnT4hpOwZ2cvBmDd7nk4q tPSxDFHArPj0aNzuP812A+F0+riV/mu1DVEn+xlFdhie4Q0bGIatIocSjo6ySkkf52uJ 2JsWUEfamrLCttzZhaOjh8LdvB934/Iozl8i+b3qrn0WqdW93QoH90r3EiZKNAMb8puy wJQA== X-Gm-Message-State: ALoCoQnAl828fcws4357HVuQEDpISfBFVoL6UgYosLAqE6Uvi/RlMGdfQe7OY2q9nq/lMt/aFSoD MIME-Version: 1.0 X-Received: by 10.202.98.193 with SMTP id w184mr9041674oib.96.1430135471492; Mon, 27 Apr 2015 04:51:11 -0700 (PDT) Sender: stedolan@stedolan.net Received: by 10.202.169.202 with HTTP; Mon, 27 Apr 2015 04:51:11 -0700 (PDT) X-Originating-IP: [128.232.9.157] In-Reply-To: References: Date: Mon, 27 Apr 2015 12:51:11 +0100 X-Google-Sender-Auth: QzPkWuTEWOv3YrKKH9v0kOZMg6M Message-ID: From: Stephen Dolan To: Jiten Pathy Cc: Jeremy Yallop , "caml-list@inria.fr" Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] phantom type 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