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 52F347EE34 for ; Mon, 28 Mar 2016 23:00:44 +0200 (CEST) IronPort-PHdr: 9a23:kkvc0RSSdBRfLe5JMTBPUBec/tpsv+yvbD5Q0YIujvd0So/mwa65YBeN2/xhgRfzUJnB7Loc0qyN4/CmAzBLuMvd+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq82VOVkD3WfhKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayV+0CQLdZFDUrNXwurI2u7EGbDFi5zH8VWWY3qlIIWFCdrULaV5LRvyL2u/BT2SSeMYXWQLk4VC7q1KxsUh7uh29HcmNhsTKftsslpbhdqQ+t7ydnwpHda4LdYPNlZqLCdNgZbW5AToBJUChQHo63b40OFvcMe+hC+drTvVwL+DSzHwXkP//ozidNj3nwlfk71eomOQ7LxgBlBM4JtGzRpdPzcqsfB7PmhJLUxCnOOqoFkQz275LFJ0l8+fw= Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=info@gerd-stolpmann.de; spf=None smtp.mailfrom=info@gerd-stolpmann.de; spf=None smtp.helo=postmaster@mout.kundenserver.de Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of info@gerd-stolpmann.de) identity=pra; client-ip=212.227.126.134; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="info@gerd-stolpmann.de"; x-sender="info@gerd-stolpmann.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of info@gerd-stolpmann.de) identity=mailfrom; client-ip=212.227.126.134; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="info@gerd-stolpmann.de"; x-sender="info@gerd-stolpmann.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mout.kundenserver.de) identity=helo; client-ip=212.227.126.134; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="info@gerd-stolpmann.de"; x-sender="postmaster@mout.kundenserver.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0DTAACrmvlWi4Z+49RdhAF9ryaLTgENgXAdhXACgSQ4FAEBAQEBAQEBEAEBAQgLCwkfMYIyghABAQQnLiQQCw4KLiE2BhMJiAkDFgEJsCdvig4NhFgBAQEBAQEEAQEBARQIhSaFPII+ggmFSwWHYYVbiXQxgTECil6BdYkzBIVUhzaHVB4BAYJWgVNqAYh5AQEB X-IPAS-Result: A0DTAACrmvlWi4Z+49RdhAF9ryaLTgENgXAdhXACgSQ4FAEBAQEBAQEBEAEBAQgLCwkfMYIyghABAQQnLiQQCw4KLiE2BhMJiAkDFgEJsCdvig4NhFgBAQEBAQEEAQEBARQIhSaFPII+ggmFSwWHYYVbiXQxgTECil6BdYkzBIVUhzaHVB4BAYJWgVNqAYh5AQEB X-IronPort-AV: E=Sophos;i="5.24,408,1454972400"; d="asc'?scan'208";a="210722272" Received: from mout.kundenserver.de ([212.227.126.134]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 28 Mar 2016 23:00:43 +0200 Received: from office1.lan.sumadev.de ([178.4.216.3]) by mrelayeu.kundenserver.de (mreue001) with ESMTPSA (Nemesis) id 0LiscI-1aAl1j16Z4-00dD2I; Mon, 28 Mar 2016 23:00:41 +0200 Received: from [192.168.65.10] (unknown [192.168.65.10]) by office1.lan.sumadev.de (Postfix) with ESMTPSA id EEFE7DC05D; Mon, 28 Mar 2016 23:00:37 +0200 (CEST) Message-ID: <1459198831.4777.28.camel@e130.lan.sumadev.de> From: Gerd Stolpmann To: Arnaud Spiwack Cc: Gabriel Scherer , Gregory Malecha , Jacques Garrigue , Mailing List OCaml Date: Mon, 28 Mar 2016 23:00:31 +0200 In-Reply-To: References: <86d1qgqu45.fsf@lpw25.net> <2D2C7D68-D59A-407B-B83A-65622DF9CC25@math.nagoya-u.ac.jp> Content-Type: multipart/signed; micalg="pgp-sha1"; protocol="application/pgp-signature"; boundary="=-/Dl+jOGx+TqeuoWGjOAn" X-Mailer: Evolution 3.10.4-0ubuntu2 Mime-Version: 1.0 X-Provags-ID: V03:K0:EOQRZoHvrvHcNDKsIQCBcG3cq9tPAYTTn2GCuCQW0yzhQdJF+SM fsTqUG3kx+AigDzMpV3pcy05COVm/tD1cqzMFpB7QiFWM1v2v0Ftw+VIXm9ptzpR9zd61nJ C5/KzgyPsoxNFku9zV3gAnjFSxFAuCZWI8HpY4bOLe6vTWjZNq/cdCShSzvhCRSAgwz3Nay hngfe/j8G2bcsGhdHCahg== X-UI-Out-Filterresults: notjunk:1;V01:K0:vDzWhPO+Vz4=:ia1TqAFPX93fSKA2BDpTeG toYB6lCM+GTYKfX2cMQsOcaWlaPFWrq2EreBgQORF+s2BRz8qd3/OSZDfzbwGOM92XYGreK2W 21YNnfJKC79UGQYWam9iyWrWiYv7qx7+deEJReX14Dd2XEZmSRdR5qwh3z3WfKIKjppADjS/+ qTzIQuxYI6w2Ol8U+8XlkxqpHwcOCQDdCCSKTp5gwKdgAGYOSpuztaJeZzQm3faEPPGXvfXw6 s4yJTPNg4czZjGLVGzzCg9Us7zazajT8taidNF3uiH5ZlarAGi9E7okEqd05TnFXPVo+o5hHY Q7i5yPxQUQ3/c2ePwHU1ecgU+c1ieflBKcksxyjmS0a/0qz1Md/tXPbFZTR+/AZoGYOq5Gbpv KadXW6EJ7Bqq5Z6TmrdEhfukxcCm2sJoLjkGKIctZJytP+cRvh1sTj0BXwNYF/mTauQ39YkC1 OlI8+EKf0Y72paMJ7dx/Ejj4YyJW38s/oTL85odGb5EGswG4pX6eAi9G94uKUh3HnaBh3zg9n pTcy6u2OWR/7RFns7ExxDNAVKu1SS6cZ+USNh8NVaL2w6OMglJjT5NiLbua7DgDsTLIGvExko C25DyMEFWDAAkxb+EkYaYW8/mIAARn7dYF8+ytbMxsovBB7V/yzIeBZ+9Sas8XhwOIftEuDGL eoMSOuKm34qYf36a7mUNMxIrBhl3/AXgQoOYqVKQDnPXdjBlGxJx7RLXXfOQolL8c1RY= Subject: Re: [Caml-list] "Type constructor b would escape its scope" --=-/Dl+jOGx+TqeuoWGjOAn Content-Type: text/plain; charset="ISO-8859-15" Content-Transfer-Encoding: quoted-printable Am Montag, den 28.03.2016, 21:20 +0200 schrieb Arnaud Spiwack: >=20 > On 28 March 2016 at 10:07, Gabriel Scherer > wrote: > (* the difference by "(type a) ..." and "type a . ..." is that > the latter > allows polymorphic recursion (just as "'a . ..."), so this > example fails > with just (type a) *) >=20=20=20=20=20=20=20=20=20 >=20=20 >=20 > So here's a question which has been nagging me for a while: is there > any occasion where one may prefer to use the `(type a)` or the `'a.` > forms over the `type a.` (apart for syntactical reasons)? If there is > I'd be really interested in seeing an example, for I can't come up > with one (especially for `(type a)`). If there aren't, what are the > obstacles to turn the `(type a)` syntax into a synonymous to the `type > a.` syntax? (I'm guessing that the `'a.` variant would be > significantly harder). Originally, I thought (type a) is just like plain 'a, only that the variable appears inside the function as abstract type. At least the manual suggests that. But looking closer, there are restrictions, and these make (type a) unattractive. E.g. # let f (x:'a) : 'a =3D match x with (p,q) -> (p,q);;=20=20=20=20=20=20=20 val f : 'a * 'b -> 'a * 'b =3D but # let f (type a) (x:a) : a =3D match x with (p,q) -> (p,q);; Error: This pattern matches values of type 'a * 'b but a pattern was expected which matches values of type a so you cannot push any constraint to it, as if it was all-quantified. Given that, the question is really whether there is any application left that could not also be expressed by "type a.". But maybe I just don't know? What about regular recursions? Tried to construct something, and I was hoping that "type a." would force me to add hinting, but to no avail: # type 'a mylist =3D Nil | Cons of 'a * 'a mylist;; # let rec last (type t) l =3D match l with Nil -> raise Not_found | Cons(x,Nil) -> x | Cons(x,l') -> last l';; val last : 'a mylist -> 'a =3D # let rec last : type t . t mylist -> t =3D fun l -> match l with Nil -> raise Not_found | Cons(x,Nil) -> x | Cons(x,l') -> last l';; val last : 'a mylist -> 'a =3D (Not that this is a good example at all, because it doesn't exploit the type name t anywhere.) Gerd --=20 ------------------------------------------------------------ Gerd Stolpmann, Darmstadt, Germany gerd@gerd-stolpmann.de My OCaml site: http://www.camlcity.org Contact details: http://www.camlcity.org/contact.html Company homepage: http://www.gerd-stolpmann.de ------------------------------------------------------------ --=-/Dl+jOGx+TqeuoWGjOAn Content-Type: application/pgp-signature; name="signature.asc" Content-Description: This is a digitally signed message part Content-Transfer-Encoding: 7bit -----BEGIN PGP SIGNATURE----- Version: GnuPG v1 iQEcBAABAgAGBQJW+ZtvAAoJEAaM4b9ZLB5TnIUH/AhrrqIKkmR0F7lfuQTQc1aM BBBV6xymkAcJlAb6+Vz37VcJuubbxM9Z6EkuWLRtwDYje+drurSHokZLuoJ+ehD/ bQrv/8MhjYfV6GflQHpVZsE2xllsJEaeVeE3A+Gks9M/gLzAcaDo89qX7GUT768G FLqeKmMRuNcfo9+09hHLLv7Vo3y1j5ZlYzN4zMu+t8Y4sQDSPOpzYAiNv0ZgcwYh NfUdHq7UGJnT5bf38cFUCzPMd5YKjIishHIdcJPjJwjlDIqX5FcoGM2KRCujypBu gZLC1L44tDHVMRsjW/8ullUUKvEgZmXoFGT+NE63Cq+eF76kLJT2WBfWiRDinN0= =hiWT -----END PGP SIGNATURE----- --=-/Dl+jOGx+TqeuoWGjOAn--