OCaml: eta-expansion?
kj
I was humming along with Jason Hickey's OCaml book, but I crashed
against a "cognitive wall" in Chapter 5, on the subject of polymorphism
and, in particular, the concepts of "value restriction" and
"eta-expansion".
I must admit that was barely holding on to the exposition in this
chapter (kinda), but Hickey finally succeeded in shaking me off
with the following:
It is usually easy to get around the value restriction by using
a technique called eta-expansion. Suppose we have an expression
e of function type. The expression (fun x -> e x) is nearly
equivalent--in fact, it is equivalent if e does not contain
side-effects. The expression (fun x -> e x) is a function, so
it is a value, and it may be polymorphic.
It is not clear to me how side-effects would cancel the equivalence
between e and (fun x -> e x). An example/counterexample would be
very helpful here.
Actually, my confusion began earlier in the chapter, where Hickey
introduces the concept of "value restriction." Even earlier he
had defined the identity function, like this:
# let identity x = x;;
So far so good. But then he asks
What happens if we apply the polymorphic identity to a value with
polymorphic function type?
...and gives as an example the following definition:
# let identity' = identity identity;;
val identity' : '_a -> '_a = <fun>
At this point all semblance of common sense evaporates, due to
something called "value restriction." Hickey explains:
...for an expression to be truly polymorphic it must be an
immutable value, which means 1) it is already fully evaluated,
and 2) it can't be modified by assignment. For example, numbers
and character constants are values. Functions are also values.
Function applications, like identity identity are *not* values,
because they can be simplified (the identity identity expression
evaluates to identity)...
What on *earth* are "function applications"? Is this something
like a promise in Scheme?
Thanks in advance for any light you may be able to shed on these
matters!
Kynn
Dan Doel
> It is not clear to me how side-effects would cancel the equivalence
> between e and (fun x -> e x). An example/counterexample would be
> very helpful here.
The case to look for is when computing e itself (not any particular e x) has
side effects. For instance (pardon if my syntax isn't valid OCaml):
val f = print "foo" ; id
versus:
fun f x = print "foo" ; id x
foo is printed once when f is computed in the first example, but delayed to
when f is called (and every time it's called) in the second case.
If you track effects with types like Haskell folk, the difference would be:
m (a -> b)
versus:
a -> m b
if that helps any. You've moved the effect until after the function
application.
I'll let people with more OCaml experience comment on the value restriction.
Dirk Thierbach
> I was humming along with Jason Hickey's OCaml book, but I crashed
> against a "cognitive wall" in Chapter 5, on the subject of polymorphism
> and, in particular, the concepts of "value restriction" and
> "eta-expansion".
> Actually, my confusion began earlier in the chapter, where Hickey
> introduces the concept of "value restriction." Even earlier he
> had defined the identity function, like this:
>
> # let identity x = x;;
>
> So far so good. But then he asks
>
> What happens if we apply the polymorphic identity to a value with
> polymorphic function type?
>
> ...and gives as an example the following definition:
>
> # let identity' = identity identity;;
> val identity' : '_a -> '_a = <fun>
>
> At this point all semblance of common sense evaporates, due to
> something called "value restriction." Hickey explains:
>
> ...for an expression to be truly polymorphic it must be an
> immutable value, which means 1) it is already fully evaluated,
> and 2) it can't be modified by assignment. For example, numbers
> and character constants are values. Functions are also values.
> Function applications, like identity identity are *not* values,
> because they can be simplified (the identity identity expression
> evaluates to identity)...
>
> What on *earth* are "function applications"? Is this something
> like a promise in Scheme?
>
> Thanks in advance for any light you may be able to shed on these
> matters!
If nobody else wants: I haven't read Hickey's book, but this value
restriction stuff is something OCaml inherited from ML. As you've
probably realized by now, mixing side-effects and lambda-calculus
naively can lead to all kinds of problems. One of these problems
is that one can use assignments to narrow down polymorphic types,
which can make the type system unsound.
Example:
$ cle ocaml
# let f = ref (fun x -> x);;
val f : ('_a -> '_a) ref = {contents = <fun>}
# let g () = !f "blah";;
val g : unit -> string = <fun>
# f;;
- : (string -> string) ref = {contents = <fun>}
# f := fun x -> x + 2;;
This expression has type string but is here used with type int
Watch how f had originally type "('_a -> '_a) ref", and after actually
applying it to a string, it changed to type "(string -> string) ref",
so the last line yields an error.
What would have happened if it got an ordinary polymorphic type, i.e.
"('a -> 'a) ref"? Then the last line would have typechecked:
# fun x -> x + 2;;
- : int -> int = <fun>
This type is an instance of "'a -> 'a", so the assigment would
succeed. If we now call g, then f contains an integer function instead
of the polymorphic function it originally had, which makes the program
crash. And the type system should prevent exactly this sort of error.
So, ML chose to make use of these special underscore types to make the
type system sound again. That's ugly, and it gets worse because the
best one can do is to approximate situations where one doesn't need
the underscore types. It looks like in the paragraph you quote,
Hickley tries to summarize the rules for it. Which is quite confusing
without knowing the context.
More info e.g. at
http://www.smlnj.org/doc/Conversion/types.html
HTH,
- Dirk
Jon Harrop
> It is not clear to me how side-effects would cancel the equivalence
> between e and (fun x -> e x). An example/counterexample would be
> very helpful here.
Consider the case when "e" is:
(print_string "foo"; print_int)
Then you have:
# (print_string "foo"; print_int);;
foo- : int -> unit = <fun>
# fun x -> (print_string "foo"; print_int) x;;
- : int -> unit = <fun>
The first printed "foo" immediately. The second did not.
> At this point all semblance of common sense evaporates, due to
> something called "value restriction."
The type of an expression can be a single as-yet-unknown type. The value
restriction protects you from accidentally using it as one type and then
another.
For example, an array containing an empty list has an unknown type
containing a non-generalized type variable that is called '_a in OCaml:
# [| [] |];;
- : '_a list array = [|[]|]
This must be done because that array element containing the empty list can
be mutated, replacing the empty list with a list containing an element. But
what is the type of that element? The element type is not yet known but it
cannot be polymorphic or we could end up with an array containing elements
of different types (which is illegal in this type system).
OCaml relaxed the usual value restriction that any unknown types must be
declared immediately and allows them to be inferred from subsequent code:
# let a = [| [] |];;
val a : '_a list array = [|[]|]
# a.(0) <- [3];;
- : unit = ()
# a;;
- : int list array = [|[3]|]
In batch compiled code, monomorphic types are not allowed to escape a
compilation unit (source file).
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?u