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#