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

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

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