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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 37E4B7ED1D for ; Sat, 3 Oct 2015 09:02:36 +0200 (CEST) IronPort-PHdr: 9a23:uWf8fxU2uqfivuoqNjY1Mab+WkHV8LGtZVwlr6E/grcLSJyIuqrYZhyPt8tkgFKBZ4jH8fUM07OQ6PC8HzJdqs/Y6DgrS99laVwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oM2PJVsVz2PkOftbF1afk0b4joEum4xsK6I8mFPig0BjXKBo/15uPk+ZhB3m5829r9ZJ+iVUvO89pYYbCf2pN4xxd7FTDSwnPmYp/4Wr8ECbFUrcrkcbB04flx4AJwne8FmuVZ70tm7+t/Fh8CicJ8z/C74uD2eM9aBuHSXvhCADLz40uEXaks1/lq8T9Aimqxt7247ZJoWYLPtxZK71YNUbWy9aV9hWViEHDJnqPNhHNPYIIesN99q1nFAJtxbrQFD0XO4= Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=rlepigre@gmail.com; spf=Pass smtp.mailfrom=rlepigre@gmail.com; spf=None smtp.helo=postmaster@mail-wi0-f177.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of rlepigre@gmail.com) identity=pra; client-ip=209.85.212.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rlepigre@gmail.com"; x-sender="rlepigre@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of rlepigre@gmail.com designates 209.85.212.177 as permitted sender) identity=mailfrom; client-ip=209.85.212.177; receiver=mail3-smtp-sop.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 (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wi0-f177.google.com) identity=helo; client-ip=209.85.212.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rlepigre@gmail.com"; x-sender="postmaster@mail-wi0-f177.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0D5AAABfQ9Wm7HUVdFVCRaDZW65ZIYnhyk8EAEBAQEBAQEBEAEBAQEBBgsLCSEugh2CIBEECwENATkDDQUVCgIFIQIRBSABBQEGHDWHdwMSBAEIpiOCBYEwPjGLR4Rlih0nDYUyAQUOgRSFUYkvg0wvgRQFlXyFF4d4giWGYZEZNYEXOGWBEAEBCAKCLm+NCAEBAQ X-IPAS-Result: A0D5AAABfQ9Wm7HUVdFVCRaDZW65ZIYnhyk8EAEBAQEBAQEBEAEBAQEBBgsLCSEugh2CIBEECwENATkDDQUVCgIFIQIRBSABBQEGHDWHdwMSBAEIpiOCBYEwPjGLR4Rlih0nDYUyAQUOgRSFUYkvg0wvgRQFlXyFF4d4giWGYZEZNYEXOGWBEAEBCAKCLm+NCAEBAQ X-IronPort-AV: E=Sophos;i="5.17,627,1437429600"; d="scan'208";a="149483042" Received: from mail-wi0-f177.google.com ([209.85.212.177]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 03 Oct 2015 09:02:35 +0200 Received: by wiclk2 with SMTP id lk2so59116134wic.0 for ; Sat, 03 Oct 2015 00:02:35 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=sender:date:from:to:subject:message-id:mime-version:content-type :content-disposition:content-transfer-encoding:user-agent; bh=EJn0cuCznAdMGlnTQJvFD42UW+Jt5LEVNULv/IItTYw=; b=DoYX/4BK4/IEMxjk9skz8Dz0weZGtknlwxmLFKaG4QMHY0Jfe5gKP4G44ao9GuniGw HGJGF1RgvEEYFmQYuKOA0U6Oj8vZ3xCXxQOpTV1VmKcNe3W4sbmzcFUqBinMR+SiRvL9 dV/uSbpuyp/MbGsJaosp+3+68AC9+VZxeH3S4Az10+u+OIyyUYGaJRsYtov5fOnNYoTU +vGAcZcMGCPuodv3pfVvifiWhbQkaFpluFwVEsPmXams4IU/HBMgDZd3uZpL5/EtRXWZ WdulWpfsvRPTUIeY35CH41oXtQoqTqUKMDTO+e061PQifCalC4MSuUvLKED8yKhjBSUg +QHg== X-Received: by 10.194.23.167 with SMTP id n7mr18968492wjf.112.1443855755338; Sat, 03 Oct 2015 00:02:35 -0700 (PDT) Received: from localhost ([84.254.185.253]) by smtp.gmail.com with ESMTPSA id ly4sm14989474wjb.4.2015.10.03.00.02.33 for (version=TLSv1.2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 03 Oct 2015 00:02:34 -0700 (PDT) Sender: Rodolphe Lepigre Date: Sat, 3 Oct 2015 09:02:26 +0200 From: Rodolphe Lepigre To: Caml List Message-ID: <20151003070226.GC22748@HPArchRod> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Disposition: inline Content-Transfer-Encoding: 8bit User-Agent: Mutt/1.5.24 (2015-08-30) Subject: [Caml-list] GADT magic Dear list, I am using a GADT and some phantom types to implement an abstract syntax tree for some functional programming language, say the λ-calculus. My first type definition was something like: ========== type valu = | LVar of string | LAbs of valu -> term and term = | Valu of valu | Appl of term * term ========== This works fine, but it is annoying to work with because of the coercion constructor "Valu". Then I decided to be to smarter and use some GADT and phantom types: ========== type v type t type _ expr = | LVar : string -> 'a expr | LAbs : (v expr -> 'b expr) -> 'a expr | Appl : 'a expr * 'b expr -> t expr type term = t expr type valu = v expr ========== This definition is much more convenient since the type "valu" is (kind of) a subtype of the type "term". It is not a real subtype since I had to define a function with the type: ========== val expr_to_term : type a. a expr -> term ========== This function is exactly the identity function, but for the type checker to accept it I need to be quite explicit: ========== let expr_to_term : type a. a expr -> term = function | LVar(x) -> LVar(x) | LAbs(f) -> LAbs(f) | Appl(t,u) -> Appl(t,u) ========== Of course, a better and more efficient implementation for this function is "Obj.magic", but this is not the question here. I was expecting the following definition to work: ========== let expr_to_term : type a. a expr -> term = function | LVar(x) -> LVar(x) | LAbs(f) -> LAbs(f) | t -> t ========== But it does not type check. This is weird because all remaining patterns captured by the "t" have type "term"... Is this normal behaviour? Is this a bug? Rodolphe -- Rodolphe Lepigre LAMA, Université Savoie Mont Blanc, FRANCE http://lama.univ-smb.fr/~lepigre/