[Caml-list] issue with polymorphism

[Caml-list] issue with polymorphism

[Guillaume Hennequin]

Dear caml-list,

let id x = x

is polymorphic, and indeed I can apply it to various types:

let _ = print_float (id 1.)
let _ = print_int (id 1)

Now, say you want to write a function that takes a function of the same ['a->'a] 
type as [id] above, and applies it to two different types:

let print_both f =
  print_int (f 1);
  print_float (f 1.0)

That in fact won't compile:

Error: This expression (1.0) has type float but an expression was expected of 
int

Naively trying to enforce polymorphism doesn't work either:

let print_both: 'a. ('a -> 'a) -> unit = fun f ->
  print_int (f 1);
  print_float (f 1.0)

As a matter of fact, neither will this:

let print1: 'a. ('a -> 'a) -> unit = fun f -> print_int (f 1)

Error: This definition has type (int -> int) -> unit
which is less general than 'a. ('a -> 'a) -> unit

What am I missing? How would you go about writing such a function?

Many thanks,
Guillaume

Re: [Caml-list] issue with polymorphism

[Gabriel Scherer]

This is possibly, but you have to write it a bit differently. See the FAQ entry,
  "How to write a function with polymorphic arguments?"
  https://ocaml.org/learn/faq.html#Howtowriteafunctionwithpolymorphicarguments

On Mon, May 16, 2016 at 11:45 AM, Guillaume Hennequin
<g.hennequin@eng.cam.ac.uk> wrote:
> Dear caml-list,
>
> let id x = x
>
> is polymorphic, and indeed I can apply it to various types:
>
> let _ = print_float (id 1.)
> let _ = print_int (id 1)
>
> Now, say you want to write a function that takes a function of the same
> ['a->'a] type as [id] above, and applies it to two different types:
>
> let print_both f =
>  print_int (f 1);
>  print_float (f 1.0)
>
> That in fact won't compile:
>
> Error: This expression (1.0) has type float but an expression was expected
> of int
>
> Naively trying to enforce polymorphism doesn't work either:
>
> let print_both: 'a. ('a -> 'a) -> unit = fun f ->
>  print_int (f 1);
>  print_float (f 1.0)
>
> As a matter of fact, neither will this:
>
> let print1: 'a. ('a -> 'a) -> unit = fun f -> print_int (f 1)
>
> Error: This definition has type (int -> int) -> unit
> which is less general than 'a. ('a -> 'a) -> unit
>
> What am I missing? How would you go about writing such a function?
>
> Many thanks,
> Guillaume
>
> --
> 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

Re: [Caml-list] issue with polymorphism

[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?

best wishes,
Guillaume

Re: [Caml-list] issue with polymorphism

[Gerd Stolpmann]

[-- Attachment #1: Type: text/plain, Size: 1042 bytes --]

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
------------------------------------------------------------


[-- Attachment #2: This is a digitally signed message part --]
[-- Type: application/pgp-signature, Size: 473 bytes --]

Re: [Caml-list] issue with polymorphism

[Yotam Barnoy]

[-- Attachment #1: Type: text/plain, Size: 1245 bytes --]

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 <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?"
> > >
> 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
> ------------------------------------------------------------
>
>

[-- Attachment #2: Type: text/html, Size: 2167 bytes --]

Re: [Caml-list] issue with polymorphism

[Gregory Malecha]

[-- Attachment #1: Type: text/plain, Size: 1679 bytes --]

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 <yotambarnoy@gmail.com> 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 <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?"
>> > >
>> 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

[-- Attachment #2: Type: text/html, Size: 2886 bytes --]

Re: [Caml-list] issue with polymorphism

[Yotam Barnoy]

[-- Attachment #1: Type: text/plain, Size: 1944 bytes --]

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 <gmalecha@gmail.com> 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 <yotambarnoy@gmail.com> 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 <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?"
>>> > >
>>> 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
>

[-- Attachment #2: Type: text/html, Size: 3528 bytes --]

Re: [Caml-list] issue with polymorphism

[Gregory Malecha]

[-- Attachment #1: Type: text/plain, Size: 2592 bytes --]

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 <yotambarnoy@gmail.com>
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 <gmalecha@gmail.com>
> 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 <yotambarnoy@gmail.com>
>> 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 <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?"
>>>> > >
>>>> 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

[-- Attachment #2: Type: text/html, Size: 4722 bytes --]

Re: [Caml-list] issue with polymorphism

[Nicolas Ojeda Bar]

[-- Attachment #1: Type: text/plain, Size: 1643 bytes --]

Hi Guillaume,

You need to use either records or objects to pass a polymorphic argument
(note that the type you want for print_both is ('a. 'a -> 'a) -> unit, not
'a. ('a -> 'a) -> unit).

For example, with objects you could do:

  let print_both (o : <f: 'a. 'a -> a>) =
    print_int (o # f 1);
    print_float (o # f 1.0)

Best wishes,
Nicolas


On Mon, May 16, 2016 at 5:45 PM, Guillaume Hennequin <
g.hennequin@eng.cam.ac.uk> wrote:

> Dear caml-list,
>
> let id x = x
>
> is polymorphic, and indeed I can apply it to various types:
>
> let _ = print_float (id 1.)
> let _ = print_int (id 1)
>
> Now, say you want to write a function that takes a function of the same
> ['a->'a] type as [id] above, and applies it to two different types:
>
> let print_both f =
>  print_int (f 1);
>  print_float (f 1.0)
>
> That in fact won't compile:
>
> Error: This expression (1.0) has type float but an expression was expected
> of int
>
> Naively trying to enforce polymorphism doesn't work either:
>
> let print_both: 'a. ('a -> 'a) -> unit = fun f ->
>  print_int (f 1);
>  print_float (f 1.0)
>
> As a matter of fact, neither will this:
>
> let print1: 'a. ('a -> 'a) -> unit = fun f -> print_int (f 1)
>
> Error: This definition has type (int -> int) -> unit
> which is less general than 'a. ('a -> 'a) -> unit
>
> What am I missing? How would you go about writing such a function?
>
> Many thanks,
> Guillaume
>
> --
> 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
>

[-- Attachment #2: Type: text/html, Size: 2702 bytes --]