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 2B6A57EE34 for ; Mon, 28 Mar 2016 22:51:38 +0200 (CEST) IronPort-PHdr: 9a23:ur3zthbwoooxggjk+wUc7KT/LSx+4OfEezUN459isYplN5qZpcuzbnLW6fgltlLVR4KTs6sC0LqG9fq8EjVdvd6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDivcePKFwV2HKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGY2zRakzTKRZATI6KCh1oZSz7ViQBTeIs1IGVGwLnlJzGwna5Rr5FsP4qTP7qeN22wGePN2wVbcwSCiv5KdtSQb1hWEJLWhq3nvQj5lUgaUTnxKguxE3l4rZZ6mRLOUkI+XbcM9MFjkJZdpYSyEUWtD0VIAIFedUeL8A94Q= Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=leo@lpw25.net; spf=None smtp.mailfrom=leo@lpw25.net; spf=None smtp.helo=postmaster@out2-smtp.messagingengine.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of leo@lpw25.net) identity=pra; client-ip=66.111.4.26; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="leo@lpw25.net"; x-sender="leo@lpw25.net"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of leo@lpw25.net) identity=mailfrom; client-ip=66.111.4.26; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="leo@lpw25.net"; x-sender="leo@lpw25.net"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@out2-smtp.messagingengine.com) identity=helo; client-ip=66.111.4.26; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="leo@lpw25.net"; x-sender="postmaster@out2-smtp.messagingengine.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0AsAQB+mPlWkhoEb0JdhH68coYNAoEkPBABAQEBAQEBARABAQEBBwsLCSEvgi2CFQEBAwEnGTkBBAsLDhMlDwEEKCGIMggErxOFLYgOg0MBAQgBAQEBARUGGYpJhAuGB5dlAY4GiSeFZI8KN4I/gVJriHoBAQE X-IPAS-Result: A0AsAQB+mPlWkhoEb0JdhH68coYNAoEkPBABAQEBAQEBARABAQEBBwsLCSEvgi2CFQEBAwEnGTkBBAsLDhMlDwEEKCGIMggErxOFLYgOg0MBAQgBAQEBARUGGYpJhAuGB5dlAY4GiSeFZI8KN4I/gVJriHoBAQE X-IronPort-AV: E=Sophos;i="5.24,408,1454972400"; d="scan'208";a="210721061" Received: from out2-smtp.messagingengine.com ([66.111.4.26]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 28 Mar 2016 22:51:37 +0200 Received: from compute1.internal (compute1.nyi.internal [10.202.2.41]) by mailout.nyi.internal (Postfix) with ESMTP id B416221BAE for ; Mon, 28 Mar 2016 16:51:34 -0400 (EDT) Received: from frontend2 ([10.202.2.161]) by compute1.internal (MEProxy); Mon, 28 Mar 2016 16:51:34 -0400 DKIM-Signature: v=1; a=rsa-sha1; c=relaxed/relaxed; d=lpw25.net; h=cc :content-type:date:from:in-reply-to:message-id:mime-version :references:subject:to:x-sasl-enc:x-sasl-enc; s=mesmtp; bh=7nd+A mN+Es8QLHT4AXEyK4wLB3k=; b=RX9KmGffKkJhdZWwdYzEc8lwjj/DWkP1rDNei OKCNUthOnyoLqbhMiMzJoRElR47jpQxBonafCGfTpPyw+tLlRe++wPmqH82X+G5q YRAF7SaHYbRMtz/If83p4evLT4ek7SJPyGy+Dqxo+W8QD6UNPYerJ90t0V1EPzhT LecDlo= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed/relaxed; d= messagingengine.com; h=cc:content-type:date:from:in-reply-to :message-id:mime-version:references:subject:to:x-sasl-enc :x-sasl-enc; s=smtpout; bh=7nd+AmN+Es8QLHT4AXEyK4wLB3k=; b=EWUTx xjU181WO1n4VcKVPFzQTloCqU6JbQcUGadnjZQ4s+/w7Y/2Yus9TV7+7J74ez0E3 cJl52JAoDHmG7LYMsGODywavABXv9FnzDoEjJvg1VuNcK0rWPknfB8NPzIf408nq ILjLIEfSBh/3Pm89unce6ybzz1Y80GZuUQbKEU= X-Sasl-enc: no6Qpkntbh/vjRzij8ITDSpiSyqXrXyp1oeQdfQzRH0c 1459198294 Received: from netbook (cpc7-walt14-2-0-cust711.13-2.cable.virginm.net [213.106.2.200]) by mail.messagingengine.com (Postfix) with ESMTPA id BB69D6801A6; Mon, 28 Mar 2016 16:51:33 -0400 (EDT) From: Leo White To: Arnaud Spiwack Cc: Gabriel Scherer , Gregory Malecha , Jacques Garrigue , Mailing List OCaml References: <86d1qgqu45.fsf@lpw25.net> <2D2C7D68-D59A-407B-B83A-65622DF9CC25@math.nagoya-u.ac.jp> X-Face: "XWxb[u_Z\PA_Y?9@|IA!!+jTb(/290-*ea/Un$I0B98.$n%eL.;2w*,z]WR#T:,p[ NBd++M7l]#7zj7!{~iw $W-"/=|dVjhT[D{4~gE}gK<2`.6fs!;uqqud]vs2N/3^m7{aS1V, Date: Mon, 28 Mar 2016 21:51:31 +0100 In-Reply-To: (Arnaud Spiwack's message of "Mon, 28 Mar 2016 21:20:55 +0200") Message-ID: <86r3euz5po.fsf@lpw25.net> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.4 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain Subject: Re: [Caml-list] "Type constructor b would escape its scope" > 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). If you don't need the polymorphism provided by `type a.` then `(type a)` might be slightly preferable because you don't need to fully describe the type of the value. For example, if you are writing a function with type `'a -> 'a` then for the first form you must write: let f : type a. a -> a = fun x -> x you cannot write: let f : type a. a -> _ = fun x -> x whereas with the second form you could write: let f (type a) (x : a) = x which infers the return type as `a` without the need to annotate it. This also illustrates what is difficult about reliably turning `(type a)` into `type a. ...`. For the second form you must work out the entire type involving `a`. Since `type a. ...` is for polymorphic recursion, you must do this before you properly type-check the body of the function. For a simple case, like: let f (x : a) : a = x it is not too bad as you can examine the argument pattern and constraint to get the full type, but as the patterns and expressions get more complicated this becomes more difficult, and at some point you are forced to draw the line and give up. Finding a sensible place to draw this line, without making inference unpredictable and confusing to users, is difficult. Regards, Leo