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 AE3F07F7AF for ; Mon, 5 Oct 2015 03:27:24 +0200 (CEST) IronPort-PHdr: 9a23:hU4BTRyirKZhpa3XCy+O+j09IxM/srCxBDY+r6Qd0OsRIJqq85mqBkHD//Il1AaPBtWHrawbwLCP6+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6OyZronLrro9X6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD89pozcNLUL37cqIkVvQYSW1+ayFm0vb2rgHORhej4X4VU2Ne0kYZQluN0BavcZ77qCr3sqJG0ymXJ8DsBeQ7UD647qpvDgTjiCodOiQR/2Tei8g2h6Ve9kGPvRt6lqzda5iIOeE2UarHZ9IVWGcJCslYTTZADZ6xR44GE+pHO+9XqJj04kZIpBD4BxH6V7Cn8SNBmnKjhf5y6O8mCwyTmVF5Eg== Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=garrigue@math.nagoya-u.ac.jp; spf=None smtp.mailfrom=garrigue@math.nagoya-u.ac.jp; spf=None smtp.helo=postmaster@mailhost.math.nagoya-u.ac.jp Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0DTAACw0RFWlwWCBoVVCRaDZW6sZJMMFwqFeQKBWBABAQEBAQEBARABAQEBAQgWB0+CHYIHAQEBAwEjBBkDASoLAQEDCwsQCAICCQgVAgJFEgYTEogHAwoHDrJOcYRrAolmA1GERQEBAQEBAQEBAQEBAQEBAQEBAQEBARABBoEih2GCboQxKTMHCoIkOxIdgRSGAwyHcIgChReIAIIdmUY4glKBai8zjQgBAQE X-IPAS-Result: A0DTAACw0RFWlwWCBoVVCRaDZW6sZJMMFwqFeQKBWBABAQEBAQEBARABAQEBAQgWB0+CHYIHAQEBAwEjBBkDASoLAQEDCwsQCAICCQgVAgJFEgYTEogHAwoHDrJOcYRrAolmA1GERQEBAQEBAQEBAQEBAQEBAQEBAQEBARABBoEih2GCboQxKTMHCoIkOxIdgRSGAwyHcIgChReIAIIdmUY4glKBai8zjQgBAQE X-IronPort-AV: E=Sophos;i="5.17,635,1437429600"; d="scan'208";a="181022685" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 05 Oct 2015 03:27:22 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id BA0756474; Mon, 5 Oct 2015 10:27:18 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (rabbit-172 [172.16.254.254]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 4B7D824D1; Mon, 5 Oct 2015 10:27:18 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= content-type:mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=iUSveLyI0yYnrxkoNRNmmUbr3DQ=; b=kyGajR6XMY3KRO5TmMqBq2zuCy+q D8jOgL8HlHCTLDDGPqysXxNdJovRPMVnl5wJTMb2zgb9+CvMr43x9ZAK7I+jc/bE CsiP+OoWXBwQcJE0bF3UCAHpNvBxEI8UIiklx0e1bIbhx+3fiI4eWDfb+m8VWb1a ApBcwrUzeqkDHc0= DomainKey-Signature: a=rsa-sha1; h=Received:Content-Type:Mime-Version:Subject:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=LAOV7x3yozgMZiObFD2Tx9mBnnjhgQYRMfmCNgnu81nJOkgSzilNBNo6x7W0MQjV9GLnYrfiewoviCkwZnbCOdOf7huYGEd6C8QkkgZc/p3eU9dJcf2qrPyWBGf47svzRLkP8fpEqVJD+hK24nKC70s7j8VTjm3WY7tGdWkI9IA=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from garrigue-mini.math.nagoya-u.ac.jp (garrigue-mini.math.nagoya-u.ac.jp [172.16.30.37]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 4DD7BDA14; Mon, 5 Oct 2015 10:26:24 +0900 (JST) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) From: Jacques Garrigue In-Reply-To: Date: Mon, 5 Oct 2015 10:27:16 +0900 Cc: Rodolphe Lepigre , Mailing List OCaml Content-Transfer-Encoding: quoted-printable Message-Id: <44040573-4A4A-40DB-9E67-A4E04054606E@math.nagoya-u.ac.jp> References: <20151003070226.GC22748@HPArchRod> To: Gabriel Scherer X-Mailer: Apple Mail (2.2104) Subject: Re: [Caml-list] GADT magic On 2015/10/03 17:54, Gabriel Scherer wrote: >=20 > 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. >=20 > (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?) Actually, I would have very little hope for the second version of expr_to_term let expr_to_term : type a. a expr -> term =3D function | LVar(x) -> LVar(x) | LAbs(f) -> LAbs(f) | t -> t The type checking algorithm never tries to infer the possible values behind a variable pattern, taking into account the other cases of the pattern-matching. The exhaustiveness check does it, but it runs after type-checking. On the other hand, one could consider handling or-patterns: let expr_to_term : type a. a expr -> term =3D function LVar _ | LAbs _ | Appl _ as t -> t The idea would be to typecheck each case separately, as somebody already suggested. Since the result is to turn expr_to_term into immediate identity, this may be worth considering. My only concern is that it may not play well with type based optimizations. Jacques Garrigue > On Sat, Oct 3, 2015 at 9:02 AM, Rodolphe Lepigre > wrote: >> Dear list, >>=20 >> 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. >>=20 >> My first type definition was something like: >>=20 >> =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 >>=20 >> 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: >>=20 >> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D >> type v >> type t >>=20 >> type _ expr =3D >> | LVar : string -> 'a expr >> | LAbs : (v expr -> 'b expr) -> 'a expr >> | Appl : 'a expr * 'b expr -> t expr >>=20 >> type term =3D t expr >> type valu =3D v expr >> =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D >>=20 >> This definition is much more convenient since the type "valu" is (kind o= f) >> a subtype of the type "term". It is not a real subtype since I had to >> define a function with the type: >>=20 >> =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 >>=20 >> This function is exactly the identity function, but for the type checker >> to accept it I need to be quite explicit: >>=20 >> =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 >>=20 >> 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: >>=20 >> =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 >>=20 >> But it does not type check. This is weird because all remaining patterns >> captured by the "t" have type "term"... >>=20 >> Is this normal behaviour? Is this a bug? >>=20 >> Rodolphe >> -- >> Rodolphe Lepigre >> LAMA, Universit=C3=A9 Savoie Mont Blanc, FRANCE >> http://lama.univ-smb.fr/~lepigre/ >>=20 >> -- >> 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