From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <jpathy@fssrv.net>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104])
	by sympa.inria.fr (Postfix) with ESMTPS id B4F987FD02
	for <caml-list@sympa.inria.fr>; Mon, 27 Apr 2015 13:32:26 +0200 (CEST)
Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  jpathy@fssrv.net) identity=pra; client-ip=209.85.212.173;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="jpathy@fssrv.net";
  x-sender="jpathy@fssrv.net"; x-conformance=sidf_compatible
Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of
  jpathy@fssrv.net designates 209.85.212.173 as permitted
  sender) identity=mailfrom; client-ip=209.85.212.173;
  receiver=mail3-smtp-sop.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 (mail3-smtp-sop.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@mail-wi0-f173.google.com) identity=helo;
  client-ip=209.85.212.173;
  receiver=mail3-smtp-sop.national.inria.fr;
  envelope-from="jpathy@fssrv.net";
  x-sender="postmaster@mail-wi0-f173.google.com";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: A0AYAgAbHT5Vm63UVdFcg19cBYMVxH2GBAKBKQc7EQEBAQEBAQERAQEBAQEGCwsJIS6EIQEBAgISEQQZAQE3AQ8LCw0CAiYCAiEBEgEFARwGEyKHdQMRDaVJPjGKSXCEYQEFiSENhUEBAQEBAQUBAQEBARcGCoEXiheCTR6BS08HgmiBRYtig1aGI4RkgVSBIj2NLYMFggYSI4EVhDceMYJEAQEB
X-IPAS-Result: A0AYAgAbHT5Vm63UVdFcg19cBYMVxH2GBAKBKQc7EQEBAQEBAQERAQEBAQEGCwsJIS6EIQEBAgISEQQZAQE3AQ8LCw0CAiYCAiEBEgEFARwGEyKHdQMRDaVJPjGKSXCEYQEFiSENhUEBAQEBAQUBAQEBARcGCoEXiheCTR6BS08HgmiBRYtig1aGI4RkgVSBIj2NLYMFggYSI4EVhDceMYJEAQEB
X-IronPort-AV: E=Sophos;i="5.11,656,1422918000"; 
   d="scan'208";a="113659077"
Received: from mail-wi0-f173.google.com ([209.85.212.173])
  by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 27 Apr 2015 13:32:26 +0200
Received: by wizk4 with SMTP id k4so95449075wiz.1
        for <caml-list@inria.fr>; Mon, 27 Apr 2015 04:32:25 -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=ulyxs4cC9xOwaVyTs3d7x+otOTwgo/WE2gwr0Tug+Ps=;
        b=N1gVmMtuyXClslfusesyKaGDqiJAB2DQRy9FIIlZqosFCUnJpBOW01sUx1wW0uz9s7
         Ur4AhnmVkajHOVPlqfDOUpSM0tMTiNn2pVDUwU/NBhmofuTuDKBUB0n9rvGyK+uBaztX
         L0wAO7dp7AKPJEiI8HQnuDJI9Fh2Kl2qjsTbs=
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=ulyxs4cC9xOwaVyTs3d7x+otOTwgo/WE2gwr0Tug+Ps=;
        b=aWuslEGwVCWMQWYrEcjF5GbcTPloao35ugpMzircraBsV/pdU6bvJiOpkod6w0P4+b
         PQANp6KtuSljJszE80geJNC3dBhlcmqEZlYUWwfmtoN6UE7Y/7Bzi3Aexqw51x9DIMky
         Stl6wK5dx0JW8WT1E8kEMAaFLB33w8SG9JJ/dFsW6x0nDH01b1b2ILRQuQzmLwtpiJmf
         hFs0gDWQfm8TsbdvCgaNZzx/jL4P1ts5MMkLKw/lH7xtXVHBi5AlwYLNDpj4UhUau6fn
         svc67yDR8B/Mk3Yahr5Hv1b5u170JAf+YDLFTvTCSzUkYlOckj3Ol4Mz8pLRq73csowk
         jyFQ==
X-Gm-Message-State: ALoCoQmh0G+fUd5zX+LZFobU8ru/wwAOnycWZrLRgQIQAw+UmAcNoMdYypNsJm/EJriWQVhpn0FG
MIME-Version: 1.0
X-Received: by 10.180.74.208 with SMTP id w16mr19779918wiv.31.1430134345830;
 Mon, 27 Apr 2015 04:32:25 -0700 (PDT)
Received: by 10.27.97.66 with HTTP; Mon, 27 Apr 2015 04:32:25 -0700 (PDT)
In-Reply-To: <CAAxsn=GiUeB17MWJVaLcu-=2E2kzP3R2cmdHR_BiEPb1Q1gu+g@mail.gmail.com>
References: <CAL2Z3DBbmv+4e+r7_9Bhbqx2yNhOXHxumxZWc1rGySb6Sr4tug@mail.gmail.com>
	<CAAxsn=GiUeB17MWJVaLcu-=2E2kzP3R2cmdHR_BiEPb1Q1gu+g@mail.gmail.com>
Date: Mon, 27 Apr 2015 04:32:25 -0700
Message-ID: <CAL2Z3DCMafiD11vrVA+gZ4W2yGxTLz_CQgfQbaVs2VsoX3D4+A@mail.gmail.com>
From: Jiten Pathy <jpathy@fssrv.net>
To: Jeremy Yallop <yallop@gmail.com>
Cc: "caml-list@inria.fr" <caml-list@inria.fr>
Content-Type: text/plain; charset=UTF-8
Subject: Re: [Caml-list] phantom type

Thanks for the reference.

On Mon, Apr 27, 2015 at 3:36 AM, Jeremy Yallop <yallop@gmail.com> wrote:
> On 27 April 2015 at 11:23, Jiten Pathy <jpathy@fssrv.net> wrote:
>> Trying to use phantom types instead of gadt for well-constructed term
>> example. Is it possible to define an evaluator eval : 'a term -> 'a
>> using phantom types?
>
> No, it's not really possible.  If the 'a parameter to 'term' is
> phantom then 'term' is defined using some other unparameterised type
> such as your 'expr':
>
>> type expr = Zero | Succ of expr | Iszero of expr;;
>
> and the problem comes down to writing a function of type
>
>    expr -> 'a
>
> which is clearly impossible.
>
> Phantom types only really help with constraints on building or
> transforming values, not with deconstructing them.
>
> However, there are various ways of writing well-typed evaluators
> without using GADTs, e.g.using a "final" encoding, which represents a
> term as an evaluation function:
>
>    Finally Tagless, Partially Evaluated:
>    http://okmij.org/ftp/tagless-final/JFP.pdf
>
> or by encoding GADTs using polymorphism:
>
>    First-class modules: hidden power and tantalizing promises
>    http://okmij.org/ftp/ML/first-class-modules/first-class-modules.pdf
>
> Jeremy.