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 49AE37ED1D for ; Sat, 3 Oct 2015 10:55:08 +0200 (CEST) IronPort-PHdr: 9a23:SdKMIxCTueggW4FsHWCwUyQJP3N1i/DPJgcQr6AfoPdwSP/5p8bcNUDSrc9gkEXOFd2CrakU16yI7uu5AjZIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/ni6bsptaKOF8ArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIZoGJ/3dKUgTLFeEC9ucyVsvJWq5i/4UBCX63AAfmITmxtOS0iZvVCpFqv25xH9uu15wCmXden7VbE7Qznqu71sRBjskCcKcTo06GDYkMFYkaRavle6rgJ4woOSbpvDZ9RkeaaIUtoQX2tMWo5qXCxMGI6mJ98ABuAbPOtc6ZL2p1YUoAGWCgylBeepwThN0CyllZYm2vgsRFmVlDcrGMgD5TGJ9dg= Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gabriel.scherer@gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer@gmail.com; spf=None smtp.helo=postmaster@mail-io0-f175.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.223.175; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.223.175 as permitted sender) identity=mailfrom; client-ip=209.85.223.175; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; 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-io0-f175.google.com) identity=helo; client-ip=209.85.223.175; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-io0-f175.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CeBADQlg9Wm6/fVdFVCRaDMDVuBqxchSGHYYYKIYV5AoEkBzwQAQEBAQEBAQEQAQEBAQEGCwsJIS6CHYIIAQECAhIRBBkBGxILAQMMBgULBQgCAgkdAgIiAREBBQEKEgYTCAoQh3YBAxINp2uBMD4xi0eBbIJ5iXcKGScDClaENgEBAQEBBQEBAQEBARYBBQ6BFIVRhH6EMSkzB4JpgUMFhX4Mj3KFF4gAgh2XehIjgRc4gi8jgV08MwEBjQYBAQE X-IPAS-Result: A0CeBADQlg9Wm6/fVdFVCRaDMDVuBqxchSGHYYYKIYV5AoEkBzwQAQEBAQEBAQEQAQEBAQEGCwsJIS6CHYIIAQECAhIRBBkBGxILAQMMBgULBQgCAgkdAgIiAREBBQEKEgYTCAoQh3YBAxINp2uBMD4xi0eBbIJ5iXcKGScDClaENgEBAQEBBQEBAQEBARYBBQ6BFIVRhH6EMSkzB4JpgUMFhX4Mj3KFF4gAgh2XehIjgRc4gi8jgV08MwEBjQYBAQE X-IronPort-AV: E=Sophos;i="5.17,627,1437429600"; d="scan'208";a="180827193" Received: from mail-io0-f175.google.com ([209.85.223.175]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 03 Oct 2015 10:55:07 +0200 Received: by ioii196 with SMTP id i196so142522821ioi.3 for ; Sat, 03 Oct 2015 01:55:06 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; bh=gHgFzCXlRCzwO3v5kPMg0EbbDyfijSOXXliUNS0fpTQ=; b=GI8r/Sh5JLK/2lQY+FMYMN9G0aZB4asiIOhEDqK+IxfgvT3dp85a2KmHSVcVIecnJH u1EgidqyQdBOiovhoWsXDnM3OT10mnfy27bKro1QU9oZ9HfVA9XZsMhxENoqcQbJCEzS 3PKvGBSfRQaLIRqAwTJdYdR+smnNGAhKevYRiAEwz5x7EJec39cqRYc9f1CJYaCqh1QO jzkSDHRZCUglebwfz8Ain/J5xBkZBw0Aqw7/MJm2sFtusDeMpSd3fIQdq2vEaKSplc4H LBvovLFJrwiOWf9ry1GkFhq1Nu7VbVBM1YYmI2tTcPwNjQTcx8Q+YdDgxJocltQdxO5x KS9g== X-Received: by 10.107.19.70 with SMTP id b67mr19226590ioj.144.1443862506119; Sat, 03 Oct 2015 01:55:06 -0700 (PDT) MIME-Version: 1.0 Received: by 10.79.19.68 with HTTP; Sat, 3 Oct 2015 01:54:26 -0700 (PDT) In-Reply-To: <20151003070226.GC22748@HPArchRod> References: <20151003070226.GC22748@HPArchRod> From: Gabriel Scherer Date: Sat, 3 Oct 2015 10:54:26 +0200 Message-ID: To: Rodolphe Lepigre Cc: Caml List Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] GADT magic This is normal behavior. You rely on the fact, when you write "| t -> t", that the remaining case is App which returns a (t term). But the type-checker will only learn this fact by opening the App constructor, which you do in the "fully explicit" version. (The type-checker is already "opening constructors" and exploring cases by itself as part of the exhaustiveness/redundancy pattern checking that Jacques Garrigue discussed at the OCaml Workshop 2015. Jacques, is there any improvement that is possible in this case without too much bakctracking?) Have you considered using polymorphic variants? They were designed for this use-case, see for example Code reuse through polymorphic variants. Jacques Garrigue, 2000 http://www.math.nagoya-u.ac.jp/~garrigue/papers/variant-reuse.pdf Le caract=C3=A8re ` =C3=A0 la rescousse - Factorisation et r=C3=A9utilisa= tion de code gr=C3=A2ce aux variants polymorphes Boris Yakobowski, 2008 http://gallium.inria.fr/~yakobows/publis/2008/jfla08.pdf On Sat, Oct 3, 2015 at 9:02 AM, Rodolphe Lepigre wrote: > Dear list, > > I am using a GADT and some phantom types to implement an abstract syntax > tree for some functional programming language, say the =CE=BB-calculus. > > My first type definition was something like: > > =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D > type valu =3D > | LVar of string > | LAbs of valu -> term > and term =3D > | Valu of valu > | Appl of term * term > =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D > > 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: > > =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D > type v > type t > > type _ expr =3D > | LVar : string -> 'a expr > | LAbs : (v expr -> 'b expr) -> 'a expr > | Appl : 'a expr * 'b expr -> t expr > > type term =3D t expr > type valu =3D v expr > =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D > > 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: > > =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D > val expr_to_term : type a. a expr -> term > =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D > > This function is exactly the identity function, but for the type checker > to accept it I need to be quite explicit: > > =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D > let expr_to_term : type a. a expr -> term =3D function > | LVar(x) -> LVar(x) > | LAbs(f) -> LAbs(f) > | Appl(t,u) -> Appl(t,u) > =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D > > 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: > > =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D > let expr_to_term : type a. a expr -> term =3D function > | LVar(x) -> LVar(x) > | LAbs(f) -> LAbs(f) > | t -> t > =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D > > 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=C3=A9 Savoie Mont Blanc, FRANCE > http://lama.univ-smb.fr/~lepigre/ > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs