Question on polymorphic typing for curried functions

Question on polymorphic typing for curried functions

[Christopher Kauffman]

I am looking for a bit of information on the behavior of curried functions wrt 
polymorphic arguments. For instance, in the following example, using a curried 
function seems to lose the nice polymorphism that I desire.

# let genf f a b = f a b;;
val genf : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = <fun>
# let specf = genf (<);;
val specf : '_a -> '_a -> bool = <fun>
# specf 1 2;;
- : bool = true
# specf;;
- : int -> int -> bool = <fun>

An alternative definition for the specific 'specf' maintains polymorphism of its 
arguments.

# let specf a b = genf (<) a b;;
val specf : 'a -> 'a -> bool = <fun>
# specf 1 2;;
- : bool = true
# specf 1.0 2.0;;
- : bool = true
# specf;;
- : 'a -> 'a -> bool = <fun>

Is there a set of rules or guidelines that determine when argument types are 
specialized versus staying polymorphic?

Cheers,
Chris

Re: [Caml-list] Question on polymorphic typing for curried functions

[Jon Harrop]

On Friday 24 August 2007 20:43:26 Christopher Kauffman wrote:
> I am looking for a bit of information on the behavior of curried functions
> wrt polymorphic arguments. For instance, in the following example, using a
> curried function seems to lose the nice polymorphism that I desire.
>
> # let genf f a b = f a b;;
> val genf : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = <fun>
> # let specf = genf (<);;
> val specf : '_a -> '_a -> bool = <fun>
> # specf 1 2;;
> - : bool = true
> # specf;;
> - : int -> int -> bool = <fun>
>
> An alternative definition for the specific 'specf' maintains polymorphism
> of its arguments.
>
> # let specf a b = genf (<) a b;;
> val specf : 'a -> 'a -> bool = <fun>
> # specf 1 2;;
> - : bool = true
> # specf 1.0 2.0;;
> - : bool = true
> # specf;;
> - : 'a -> 'a -> bool = <fun>
>
> Is there a set of rules or guidelines that determine when argument types
> are specialized versus staying polymorphic?

Yes. If you partially apply then you get a monomorphic result:

# genf (<);;
- : '_a -> '_a -> bool = <fun>

If you then wrap that in any kind of closure then it becomes polymorphic 
again:

# (fun a -> genf (<));;
- : 'a -> 'b -> 'b -> bool = <fun>

-- 
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
OCaml for Scientists
http://www.ffconsultancy.com/products/ocaml_for_scientists/?e

Re: [Caml-list] Question on polymorphic typing for curried functions

[Julien Moutinho]

On Fri, Aug 24, 2007 at 02:43:26PM -0500, Christopher Kauffman wrote:
> I am looking for a bit of information on the behavior of curried functions 
> wrt polymorphic arguments. For instance, in the following example, using a 
> curried function seems to lose the nice polymorphism that I desire.
> [...]
> Is there a set of rules or guidelines that determine when argument types 
> are specialized versus staying polymorphic?

This may be of interest to you:
http://caml.inria.fr/pub/old_caml_site/FAQ/FAQ_EXPERT-eng.html#eta_expansion

RE: [Caml-list] Question on polymorphic typing for curried functions

[Harrison, John R]

Hi Chris,

| I am looking for a bit of information on the behavior of
| curried functions wrt polymorphic arguments. For instance, in
| the following example, using a curried function seems to lose
| the nice polymorphism that I desire.

OCaml uses a variant of the so-called "value restriction" to ensure
soundness in the way polymorphism and imperative features interact.
You can find more information in this paper by Jacques Garrigue:

  http://www.math.nagoya-u.ac.jp/~garrigue/papers/morepoly-long.pdf

It can sometimes be annoying and unintuitive (for me anyway) to lose
polymorphism by eta contraction. But this approach is at least
relatively simple and well-understood.

John.