0

I am starting to learn OCaml and was trying to do some practices:

# let left x y = x;;
val left : 'a -> 'b -> 'a = <fun>

# let first = List.fold_right left;;
val first : '_a list -> '_a -> '_a = <fun>

Why is first only weakly polymorphic instead of fully polymorphic?

TwiNight
  • 1,852
  • 1
  • 17
  • 27
  • 1
    possible duplicate of [What is the difference between 'a and '\_l?](http://stackoverflow.com/questions/4242677/what-is-the-difference-between-a-and-l) – ivg Oct 08 '14 at 22:49
  • try to search SO for "ocaml value restriction", there're plenty of good answers. – ivg Oct 08 '14 at 22:51
  • 1
    And I like this answer http://stackoverflow.com/a/22507665/2625442 – ivg Oct 08 '14 at 22:54

1 Answers1

1

This is the value restriction. first is not a value, it's a function application.

To get a fully polymorphic version, use eta expansion:

# let left x y = x;;
val left : 'a -> 'b -> 'a = <fun>
# let first a b = List.fold_right left a b;;
val first : 'a list -> 'a -> 'a = <fun>

As @ivg points out, this is a commonly asked OCaml question.

Update

Here's a function application that's unsafe to generalize:

# let f x = ref x;;
val f : 'a -> 'a ref = <fun>
# f [];;
- : '_a list ref = {contents = []}

If you pretend that the result has the type 'a list ref you can make the code go wrong (I tried it).

Here's a partial application that's unsafe to generalize:

# let g x = let z = ref x in fun () -> z;;
val g : 'a -> unit -> 'a ref = <fun>
# g [];;
- : unit -> '_a list ref = <fun>

If you pretend that the result has type unit -> 'a list ref you can make this code go wrong (I tried it).

Jeffrey Scofield
  • 65,646
  • 2
  • 72
  • 108
  • Actually, can you please explain to me what is the harmness in this case if value restriction was not there, say `let first = List.fold_right left` become `val first: 'a list -> 'a -> 'a = `? – Jackson Tale Oct 09 '14 at 09:55
  • Or give an example of partial application would fail without value restriction? – Jackson Tale Oct 09 '14 at 10:21
  • or the reason value restriction is there is because of allowing imperative / ref? – Jackson Tale Oct 09 '14 at 10:33
  • 1
    Yes, the value restriction is there because of `ref`. That's why pure languages like Haskell don't have this restriction. – Tarmil Oct 09 '14 at 11:29
  • @Tarmil I understand why value restriction is necessary, but I can't see why partial function application would need value restriction. Can you construct a situation where partial application could break things if there is no value restriction? – TwiNight Oct 09 '14 at 20:07
  • A partial application is really just an application that returns a function. There's nothing particularly special about partial applications. No application (partial or not) is a value in the sense of the value restriction. – Jeffrey Scofield Oct 09 '14 at 20:20