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 3F5307EE45 for ; Tue, 4 Jun 2013 11:23:42 +0200 (CEST) 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.214.47; 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.214.47 as permitted sender) identity=mailfrom; client-ip=209.85.214.47; 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-bk0-f47.google.com) identity=helo; client-ip=209.85.214.47; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-bk0-f47.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArgAAPKwrVHRVdYvjWdsb2JhbABZgzm/CXoIFg4BAQEBBwsLCRIGJIIjAQEFJxkBGx0BAwwGBQsDCi4hAQERAQUBHAYTh3oBAw8Mnl+MSoJ9hRMKGScNWIguAQUMjECCWgeDWAOVWIFmgSmKdIM+FimENzo X-IPAS-Result: ArgAAPKwrVHRVdYvjWdsb2JhbABZgzm/CXoIFg4BAQEBBwsLCRIGJIIjAQEFJxkBGx0BAwwGBQsDCi4hAQERAQUBHAYTh3oBAw8Mnl+MSoJ9hRMKGScNWIguAQUMjECCWgeDWAOVWIFmgSmKdIM+FimENzo X-IronPort-AV: E=Sophos;i="4.87,798,1363129200"; d="scan'208";a="20216158" Received: from mail-bk0-f47.google.com ([209.85.214.47]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 04 Jun 2013 11:23:41 +0200 Received: by mail-bk0-f47.google.com with SMTP id jg9so2093625bkc.6 for ; Tue, 04 Jun 2013 02:23:41 -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; bh=lh0kaThtg/A6/eDmlQfFzR2ImFeNXF8A5hO53ySD5z4=; b=p86nuN55iA6c2HnuMr5dbulxoo7hWfBn/7DWSvmrNgxz24dV25AQcYjxzfG6BZ3AOP FRUnpK+lRznJc3Vvb09nDhIZkftYuii2r59aXsMefQOutl8XqSbhyXUP4jWZN0FZpozq Gp2TdZ8XayM/NGxyaEWZ8tlJ66L3fgB8PVEJAeQYMB6G5otSmsUND7iACbEE45jXvSEm T9Iw6nSLhGTdgS/8IQxWFXetnA8Fg1eGhaXoHtWZsiptRAjh8/Q6D6u1KJA2ZpTeVK5j XGceYvBU3M47zHeMzs+0IKwjEMnDz8G7T2uQ3tKbWm8IrZtwgceG3+hSetrCksWdzjFt mVow== X-Received: by 10.204.240.15 with SMTP id ky15mr5724489bkb.144.1370337821173; Tue, 04 Jun 2013 02:23:41 -0700 (PDT) MIME-Version: 1.0 Received: by 10.204.35.75 with HTTP; Tue, 4 Jun 2013 02:23:01 -0700 (PDT) In-Reply-To: <87a9n6s5jo.fsf@golf.niidar.ru> References: <87ehciseni.fsf@golf.niidar.ru> <87a9n6s5jo.fsf@golf.niidar.ru> From: Gabriel Scherer Date: Tue, 4 Jun 2013 11:23:01 +0200 Message-ID: To: Ivan Gotovchits Cc: caml-list@inria.fr Content-Type: text/plain; charset=ISO-8859-1 Subject: Re: [Caml-list] GADT and locally ADT In expressions, type variables 'a 'b do not enforce polymorphism, they are merely name for types that will be inferred. let f : 'a -> 'a = fun x -> x + 1 is accepted. So your second example with ('a, 'b) does not enforce polymorphism. This is not in general a problem as if the inferred type is indeed a type variable, it will be generalized by the inference algorithm and therefore "turned into polymorphism" after type inference. It is problematic however for polymorphic recursive functions (this form of polymorphism would have to be "guessed" before the recursive definition is type-checked, and therefore requires an annotation), and for GADTs. There are two *distinct* notions used to enforce polymorphism: - polymorphic type variables as in val f : 'a -> 'a or let f : 'a . 'a -> 'a = ... (useful for polymorphic recursion) - local abstract types let f (type t) : t -> t = ... fun (type t) -> ... (useful for GADTs) Local abstract types are documented in http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#toc80 . They are not type variable (they cannot be unified with anything, hence enforce polymorphism), but type "constructors" syntactically (like 'list' in ('a list), but without a parameter). We say that GADTs introduce equations and refine types; they can only refine local abstract types, not type variables. The refinement of GADT types is similar to what happen when you traverse a module abstraction, outside you know the abstract type M.t, and inside you know (type M.t = int). Due to this "implementation detail" of GADTs, the following code (that enforces polymorphism) would still fail to type-check: let f : 'b . ('a, 'b) access -> unit = function | ReadWrite ch -> () | Read ch -> () while the following work let f (type t) : ('a, t) access -> unit = function | ReadWrite ch -> () | Read ch -> () Finally, the syntax let f : type t . ('a, t) acc -> unit = function ... is a merge of both ('a 'b . ...) and ((type t) ...): it provides a local type constructor, and enables polymorphic recursion. This is what you should use when you write recursive functions using GADTs. On Tue, Jun 4, 2013 at 9:23 AM, Ivan Gotovchits wrote: > Gabriel Scherer writes: > >> If the function knows (or infer) that the argument type is (ro), then >> there is only one case to handle. But there is also a function that is >> polymorphic over the second argument, and it must be callable with >> both (ro) and (rw) values : this function works "for any access mode". >> This is what the annotated function >> >>> let f (type t) (inp: ('a,t) access) = match inp with >>> | ReadWrite (ch) -> () >>> | Read (ch) -> ();; >> >> does. > > Looks reasonable, but can you, please, explain the difference between > function: > > let f (type t) (inp: ('a,t) access) = match inp with > | ReadWrite ch -> () > | Read ch -> () > > that have type > > val f : ('a, 'b) access -> unit > > and > > let f (inp: ('a,'b) access) = match inp with > | ReadWrite ch -> () > | Read ch -> () > > that fails to type check: > > Error: This pattern matches values of type ('a, ro) access > but a pattern was expected which matches values of type > ('a, rw) access