Binding and evaluation order in module/type/value languages

Binding and evaluation order in module/type/value languages

[Dawid Toton]

Thinking about the discussion in the recent thread "Phantom types" [1],
I have created the following piece of code that aims to demonstrate
binding and evaluation order that takes effect in all three levels of OCaml.

My question is: what are the precise rules is the case of type language?
I have impression that it is lazy and memoized evaluation. But this my
guess looks suspicious.

I don't intend this question to be about inner working of the compiler,
but about the definition at the conceptual level.


(* 1. Module language; side effect = create fresh record type; test =
type equality test *)

module type T = sig type t end
module R (T:T) = struct type r = {lab : int} end

module TF = struct type t = float end
module TS = struct type t = string end
module R1 = R(TF)
module R2 = R(TF)
module R3 = R(TS)

let test12 (k : R1.r) (l : R2.r) = (k=l) (* pass => R1.r = R2.r *)
let test13 (k : R1.r) (l : R3.r) = (k=l) (* pass => R1.r = R3.r *)

(* Conclusion: RHS evaluated at the mapping definition point *)

(* 2. Type language; side effect = create fresh record type; test = type
equality test *)

type 't r = {lab : int}

type tf = float
type ts = string
type r1 = tf r
type r2 = tf r
type r3 = ts r

let test12 (k : r1) (l : r2) = (k=l) (* pass => r1 = r2 *)
let test13 (k : r1) (l : r3) = (k=l) (* fail => r1 ≠ r3 *)

(* Conclusion: RHS evaluated some time after the mapping is applied;
sort of memoization at the conceptual level *)

(* 3. Value language; side effect = create fresh int; test = value
equality test *)
let r t = Oo.id (object end)

let tf = 0.
let ts = "A"
let r1 = r tf
let r2 = r tf
let r3 = r ts

let test12 = assert (r1 = r2) (* fail => r1 ≠ r2 *)
let test13 = assert (r1 = r3) (* fail => r1 ≠ r3 *)

(* Conclusion: RHS evaluated exactly at the point of mapping application *)

Dawid

[1]
http://groups.google.com/group/fa.caml/browse_thread/thread/0df560ee78e0f75f#

Re: [Caml-list] Binding and evaluation order in module/type/value languages

[Jacques Garrigue]

From: Dawid Toton <d0@wp.pl>
> Thinking about the discussion in the recent thread "Phantom types" [1],
> I have created the following piece of code that aims to demonstrate
> binding and evaluation order that takes effect in all three levels of OCaml.
> 
> My question is: what are the precise rules is the case of type language?
> I have impression that it is lazy and memoized evaluation. But this my
> guess looks suspicious.
> 
> I don't intend this question to be about inner working of the compiler,
> but about the definition at the conceptual level.

It is not clear that this will work at all.
The semantics of ocaml (contrary to SML) is not defined in terms of
type generativity.

> (* 1. Module language; side effect = create fresh record type; test =
> type equality test *)
> 
> module type T = sig type t end
> module R (T:T) = struct type r = {lab : int} end
> 
> module TF = struct type t = float end
> module TS = struct type t = string end
> module R1 = R(TF)
> module R2 = R(TF)
> module R3 = R(TS)
> 
> let test12 (k : R1.r) (l : R2.r) = (k=l) (* pass => R1.r = R2.r *)
> let test13 (k : R1.r) (l : R3.r) = (k=l) (* pass => R1.r = R3.r *)
> 
> (* Conclusion: RHS evaluated at the mapping definition point *)

Wrong: test13 fails.
OCaml functors are applicative, and type equality is the equality of
paths.
Stranger: defining twice TF, or defining an alias for TF, will result
in different types.

module TF' = TF
module R4 = R(TF')
let f (x : R1.r) = (x : R4.r);;
Error: This expression has type R1.r = R(TF).r
       but an expression was expected of type R4.r = R(TF').r

So your comment for the type language applies here:
> (* Conclusion: RHS evaluated some time after the mapping is applied;
> sort of memoization at the conceptual level *)
I'm not sure there is a timing here, but there is certainly some form
of memoization, which happens to be done by name.

> (* 2. Type language; side effect = create fresh record type; test = type
> equality test *)
> 
> type 't r = {lab : int}
> 
> type tf = float
> type ts = string
> type r1 = tf r
> type r2 = tf r
> type r3 = ts r
> 
> let test12 (k : r1) (l : r2) = (k=l) (* pass => r1 = r2 *)
> let test13 (k : r1) (l : r3) = (k=l) (* fail => r1 ≠ r3 *)
> 
> (* Conclusion: RHS evaluated some time after the mapping is applied;
> sort of memoization at the conceptual level *)

Lots of people seem to think that generativity of type definitions
gives you phantom types. This is true in Haskell, but not in ocaml.

# let f x = (x : r1 :> r3);;
val f : r1 -> r3 = <fun>

So r1 and r3 are not strictly equal, but they are equivalent from the
point of view of subtyping.
Please do not use this approach for phantom types, except if you want
the ability to forget the argument where desired.
As written in other mails, the right approach for phantom types is to
use private types, as you can control the variance of their
parameters.

Conclusion: in the type language, this is more like you thought at
first for functors, i.e. RHS evaluated at the mapping definition point.
But if the RHS is abstract/private or includes the type parameters,
then they are involved in deciding the equality (structurally, not
through generativity).

> (* 3. Value language; side effect = create fresh int; test = value
> equality test *)
> let r t = Oo.id (object end)
> 
> let tf = 0.
> let ts = "A"
> let r1 = r tf
> let r2 = r tf
> let r3 = r ts
> 
> let test12 = assert (r1 = r2) (* fail => r1 ≠ r2 *)
> let test13 = assert (r1 = r3) (* fail => r1 ≠ r3 *)
> 
> (* Conclusion: RHS evaluated exactly at the point of mapping application *)

Sure, this is an eager language.

Jacques Garrigue

Re: Binding and evaluation order in module/type/value languages

[Dawid Toton]

> It is not clear that this will work at all.
> The semantics of ocaml (contrary to SML) is not defined in terms of
> type generativity.
>
>   
This is great eureka to me.
I thought that when the compiler refuses to unify some types it knows
that they are incompatible (as the error message says).
But now I think (as I currently understand non-generativity) that
sometimes the compiler simply doesn't know if some types are equal and
avoids unification of such types. The error message should be instead:
"Cannot unify the following types, because I don't have any proof that
they are equal (and I don't have looked for the proof really hard)..."

So in order to have not unifiable phantom types one has to kind of trick
the compiler and hide the fact that they are equal.

Dawid