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 BE4C07EE79 for ; Mon, 16 May 2016 21:10:22 +0200 (CEST) IronPort-PHdr: 9a23:1nYjzxVZly+pTAng+0MHzJ5ZpuLV8LGtZVwlr6E/grcLSJyIuqrYZhyHt8tkgFKBZ4jH8fUM07OQ6PCxHzZeqs/a6DgrS99laVwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oM2CJV8Wz2PmOftbF1afk0b4joEum4xsK6I8mFPig0BjXKBo/15uPk+ZhB3m5829r9ZJ+iVUvO89pYYbCf2pN4xxd7FTDSwnPmYp/4Wr8ECbFUrcrkcbB1QRjhNNSyLM9hf9T9+loyzmv+930TOcOtzeQrU9WDDk5KBuHkzGkiACYhEj/W7QkN04qatfrRmhrlQrzIvdZIyeNPNWcabUfNdcTm1ECJUCHxddC5+xOtNcR9EKOvxV+syk/wMD Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gmalecha@gmail.com; spf=Pass smtp.mailfrom=gmalecha@gmail.com; spf=None smtp.helo=postmaster@mail-oi0-f53.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gmalecha@gmail.com) identity=pra; client-ip=209.85.218.53; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gmalecha@gmail.com"; x-sender="gmalecha@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gmalecha@gmail.com designates 209.85.218.53 as permitted sender) identity=mailfrom; client-ip=209.85.218.53; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gmalecha@gmail.com"; x-sender="gmalecha@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-oi0-f53.google.com) identity=helo; client-ip=209.85.218.53; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gmalecha@gmail.com"; x-sender="postmaster@mail-oi0-f53.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0DjAAC0GTpXjzXaVdFchAx+BrIPgmGFBYF2JIVtAoEnBzoSAQEBAQEBAQERAQEBAQcLCwkhL4ItghUBAQEDARIRBBkBFAcPDgEDAQsGAwILDSoCAiEBAREBBQEcBhMJGYdyAQMPCA6SAY9CgTE+MYs7gWqCWAWHVgoZJw1Sg1UBAQEBAQEBAQEBAQEBAQEBAQEBAQEUAgYQhR14hE2CQ4IIIYJTglkFh36GVYkjMYV+hicDgXaCN4xih1yGJxIegQ4PGAiCLB6BdRwyAYgFAQEB X-IPAS-Result: A0DjAAC0GTpXjzXaVdFchAx+BrIPgmGFBYF2JIVtAoEnBzoSAQEBAQEBAQERAQEBAQcLCwkhL4ItghUBAQEDARIRBBkBFAcPDgEDAQsGAwILDSoCAiEBAREBBQEcBhMJGYdyAQMPCA6SAY9CgTE+MYs7gWqCWAWHVgoZJw1Sg1UBAQEBAQEBAQEBAQEBAQEBAQEBAQEUAgYQhR14hE2CQ4IIIYJTglkFh36GVYkjMYV+hicDgXaCN4xih1yGJxIegQ4PGAiCLB6BdRwyAYgFAQEB X-IronPort-AV: E=Sophos;i="5.26,627,1459807200"; d="scan'208,217";a="218446296" Received: from mail-oi0-f53.google.com ([209.85.218.53]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 16 May 2016 21:10:21 +0200 Received: by mail-oi0-f53.google.com with SMTP id k142so283672782oib.1 for ; Mon, 16 May 2016 12:10:21 -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; bh=w/D9SYJzp1048os9RcN6pyKPBoF7nKL523vRMezQ5e8=; b=UBGJvGvz1Ls4AZ6/Yrsi+NRixu8yJ/mMsxnGzX3ddmswMXnM2lvcU1AOzKegS4wVEY U5gd/nZ4M2zTkPAZ1tawt8I+FhBb2aJBXovK5IusWjM17WjLVRE4PvZp/lXcykNUJpMK bCLcypXQbVONHvP8mAmFZdJSWETmslYL38m5UvfPmLK41fuseG3rsCbVKvqzPgsKs/Vg 1sbBPryTj6lIZYHoDxwjX6do/pbS2tuE7p3nV9jrXDWHzMarfqoa7Z/VDhDByGnKdhk3 M9TI5LGM2tKPeLlZ54YA25Rns1MMEm8kETBSF7UhMUU7MB73plr2fNgOyhC8E72Kj+Fl ViLw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=w/D9SYJzp1048os9RcN6pyKPBoF7nKL523vRMezQ5e8=; b=eUxEGc80ZWB84nIVxcmKH377EymsOl0LuOt6QEX5IMuK1bqQFjhc6bl5hTyXIifbLg WvWCHDWpRurilXphNFU9C8wqhZV7tiCZiur2hFSjKqxa5mlyVel5Py616zLYcGdfDlG5 IsVKLRwTuaYnj3hWV5gydS8CLgalEKz/GWUKBAaWDADMp4mXFUMfY4+aN9AS2z+b9dFr nqM4mvzFRDjYkjOD1jpQdOHoVWXzuCZl6Gq58e8eFsVc92+PuhlhiQXSxGp0NGB6lFDg 2hEJzzFdmxPiiLNujLdxEWG7bxnulljcznQEqKroJabYxc/m3xbYWgNBwWCDVHdn/0mz 2JBw== X-Gm-Message-State: AOPr4FX9fxywzLg6rDEUbqvAn4uclc+SAbzrpfsROjVD17ok0dStdZJysMCdTWjDAC1F1EroX5IdnuIhZN9U+A== X-Received: by 10.157.43.29 with SMTP id o29mr6960365otb.94.1463425820160; Mon, 16 May 2016 12:10:20 -0700 (PDT) MIME-Version: 1.0 Received: by 10.157.20.211 with HTTP; Mon, 16 May 2016 12:09:40 -0700 (PDT) In-Reply-To: References: <1463412482-sup-8520@hennequin-xps> <1463417600-sup-2106@hennequin-xps> <1463419945.3467.32.camel@e130.lan.sumadev.de> From: Gregory Malecha Date: Mon, 16 May 2016 12:09:40 -0700 Message-ID: To: Yotam Barnoy Cc: Gerd Stolpmann , Guillaume Hennequin , caml users Content-Type: multipart/alternative; boundary=001a1141da402a78e80532fa6092 Subject: Re: [Caml-list] issue with polymorphism --001a1141da402a78e80532fa6092 Content-Type: text/plain; charset=UTF-8 I'm not 100% familiar with the object system, but you can write them on records. type 'a stream = { fold : 'b . ('a -> 'b -> 'b) -> 'b -> 'b } The reason that writing them here does not break inference is that the inference mechanism knows that it needs to insert the universally quantified type at the position of the record constructor, i.e. when it sees { foo = X } it knows that it should introduce the quantifier there. This makes it syntax-directed. On Mon, May 16, 2016 at 12:04 PM, Yotam Barnoy wrote: > Right, but they can't be inferred on objects and records either, and yet > they're allowed there... so what was the rationale? > > On Mon, May 16, 2016 at 2:53 PM, Gregory Malecha > wrote: > >> There may other reasons as well, e.g. performance and compilability, but >> the main reason that I know is that inferring these types is difficult >> (undecideable in general). For a point of comparison, GHC supports types >> like this, but only when they are explicitly written. >> >> On Mon, May 16, 2016, 11:50 AM Yotam Barnoy >> wrote: >> >>> Paging the type experts -- is there a concrete reason why we disallow >>> writing this type directly? >>> >>> On Mon, May 16, 2016 at 1:32 PM, Gerd Stolpmann >>> wrote: >>> >>>> Am Montag, den 16.05.2016, 17:55 +0100 schrieb Guillaume Hennequin: >>>> > Thanks all for your prompt answers; >>>> > >>>> > > See the FAQ entry, "How to write a function with polymorphic >>>> arguments?" >>>> > > >>>> https://ocaml.org/learn/faq.html#Howtowriteafunctionwithpolymorphicarguments >>>> > >>>> > this page explains how to do it with records or objects, but ends >>>> with a >>>> > mysterious "FIXME: a direct way now exists". Does anyone know what >>>> this might >>>> > refer to? >>>> >>>> What you would need is >>>> >>>> let print_both : ('a . 'a -> 'a) -> unit = ... >>>> >>>> i.e. the scope of the quantifier is restricted to the first argument. >>>> This doesn't exist to my knowledge. Maybe it was part of some dev >>>> version? >>>> >>>> Gerd >>>> -- >>>> ------------------------------------------------------------ >>>> 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 >>>> ------------------------------------------------------------ >>>> >>>> >>> -- >> >> - gregory malecha >> gmalecha.github.io >> > > -- gregory malecha gmalecha.github.io --001a1141da402a78e80532fa6092 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
I'm not 100% familiar with the object system, but you = can write them on records.

type 'a stream =3D { fold : 'b . ('a -> 'b -> = 'b) -> 'b -> 'b }

The rea= son that writing them here does not break inference is that the inference m= echanism knows that it needs to insert the universally quantified type at t= he position of the record constructor, i.e. when it sees { foo =3D X } it k= nows that it should introduce the quantifier there. This makes it syntax-di= rected.



<= div class=3D"gmail_quote">On Mon, May 16, 2016 at 12:04 PM, Yotam Barnoy <yotambarnoy@gmail.com> wrote:
Right, but they can't be inferred on objects an= d records either, and yet they're allowed there... so what was the rati= onale?

O= n Mon, May 16, 2016 at 2:53 PM, Gregory Malecha <gmalecha@gmail.com&g= t; wrote:

There may= other reasons as well, e.g. performance and compilability, but the main re= ason that I know is that inferring these types is difficult (undecideable i= n general). For a point of comparison, GHC supports types like this, but on= ly when they are explicitly written.


On Mon, May 16, 2016, 11:50= AM Yotam Barnoy <yotambarnoy@gmail.com> wrote:
Paging the type experts -- is there a concrete reas= on why we disallow writing this type directly?

On Mon, May 16, 2016 at 1:32 PM, Gerd St= olpmann <info@gerd-stolpmann.de> wrote:
Am Montag, den 16.05.2016, 17:55 +0100 schrieb Guillaume= Hennequin:
> Thanks all for your prompt answers;
>
> > See the FAQ entry, "How to write a function with polymorphic= arguments?"
> >=C2=A0 =C2=A0ht= tps://ocaml.org/learn/faq.html#Howtowriteafunctionwithpolymorphicarguments<= /a>
>
> this page explains how to do it with records or objects, but ends with= a
> mysterious "FIXME: a direct way now exists". Does anyone kno= w what this might
> refer to?

What you would need is

let print_both : ('a . 'a -> 'a) -> unit =3D ...

i.e. the scope of the quantifier is restricted to the first argument.
This doesn't exist to my knowledge. Maybe it was part of some dev
version?

Gerd
--
------------------------------------------------------------
Gerd Stolpmann, Darmstadt, Germany=C2=A0 =C2=A0 gerd@gerd-stolpmann.de
My OCaml site:=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 http://www.camlcity.org<= br> Contact details:=C2=A0 =C2=A0 =C2=A0 =C2=A0 http://www.camlcity.= org/contact.html
Company homepage:=C2=A0 =C2=A0 =C2=A0 =C2=A0http://www.gerd-stolpmann.de=
------------------------------------------------------------


--

- gregory malecha
=C2=A0 gmalecha.git= hub.io





--
gregory malecha
--001a1141da402a78e80532fa6092--