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

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#