From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 C62737FCCB for ; Mon, 27 Apr 2015 12:23:48 +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.171; 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.171 as permitted sender) identity=mailfrom; client-ip=209.85.212.171; 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-f171.google.com) identity=helo; client-ip=209.85.212.171; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="jpathy@fssrv.net"; x-sender="postmaster@mail-wi0-f171.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0AvAgDFDT5VlKvUVdFchDsFgxXDKoh/BzoSAQEBAQEBAREBAQEBBwsLCR8whDkRBBkBATglDwImAiQSAQUBFgwbGogJpSg+MYpJcIRhAQWPFAYKgReSC4FFi2KQMZQXEiOBFYQ3HjGCRAEBAQ X-IPAS-Result: A0AvAgDFDT5VlKvUVdFchDsFgxXDKoh/BzoSAQEBAQEBAREBAQEBBwsLCR8whDkRBBkBATglDwImAiQSAQUBFgwbGogJpSg+MYpJcIRhAQWPFAYKgReSC4FFi2KQMZQXEiOBFYQ3HjGCRAEBAQ X-IronPort-AV: E=Sophos;i="5.11,656,1422918000"; d="scan'208";a="113651572" Received: from mail-wi0-f171.google.com ([209.85.212.171]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 27 Apr 2015 12:23:48 +0200 Received: by widdi4 with SMTP id di4so93248318wid.0 for ; Mon, 27 Apr 2015 03:23:47 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=fssrv.net; s=google; h=mime-version:date:message-id:subject:from:to:content-type; bh=84GXxKgfiib3Q6NgrGmOEcS1GjH0EZNhsIzWOo02Vs0=; b=TJ03sToLCK4hfqL+nfFDFRcd8yBwJhfSJEjN05s8MRTVUh7jXyAKQZKjYcTXHJhE3v EPr2y7zkP1267maP6kiXC/k6blj8ze4AjaVFPVMx09eE3xZ9xzlf2eg96V6Pakbm4Q47 BJ93V7Sq0k5oYe1WOSm7pkB9kWHRRrB/koGnY= X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:date:message-id:subject:from:to :content-type; bh=84GXxKgfiib3Q6NgrGmOEcS1GjH0EZNhsIzWOo02Vs0=; b=YnH7bz1jimXQzOc373Y4qET5RzuG93BFyyHHTRCwcSE9cq5Sc8OEYwbUvkSRpw+tOn JusCP7UB5AZGuVTgw55z98q8ij2ZZ4Bz07ZsnXPKjjY6dvao0os2XelbGLZ4zG4Tcy0B mIm/DjvbV1Keyt2G2BjRo5ieG+RD6Opwq+JJLk3n86/oRf722pQ0BUZ0I/yrbQtlzL40 6A/t9CZRj0j1hX1d7fBoiilGvJJp95TDAO06t84OT9XCNFTB3Pf07g3llP3KugZU2rXB HMK1M4Ut8pcVSxj2OMH+uZNexwXhdVlo8FthyAg/dwkIV6tEtQOvjZ9sK1XvQsJ1TnU8 GxqQ== X-Gm-Message-State: ALoCoQkiozES4/rFqO3wLoKCk8qxf8HQZCqt999VYXoDLwWzejatZ3kXsGdgf0mandsAfsSBgMjk MIME-Version: 1.0 X-Received: by 10.180.101.3 with SMTP id fc3mr18958120wib.47.1430130227854; Mon, 27 Apr 2015 03:23:47 -0700 (PDT) Received: by 10.27.97.66 with HTTP; Mon, 27 Apr 2015 03:23:47 -0700 (PDT) Date: Mon, 27 Apr 2015 03:23:47 -0700 Message-ID: From: Jiten Pathy To: "caml-list@inria.fr" Content-Type: text/plain; charset=UTF-8 Subject: [Caml-list] phantom type Hello, 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? Something like following doesn't work. type expr = Zero | Succ of expr | Iszero of expr;; type 'a term = Expr of expr;; (* ways to construct a term *) let zero : int term = Expr Zero;; let succ : int term -> int term = fun (Expr x) -> Expr (Succ x);; let iszero : int term -> bool term = fun (Expr x) -> Expr (Iszero x);; let rec eval : 'a.'a term -> 'a = fun (type a) (t : a term) -> match t with | Expr Zero -> 0 | Expr (Succ e) -> eval (Expr e) + 1 | Expr (Iszero e) -> if (eval (Expr e) == 0) then true else false ;;