From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <d0@wp.pl>
X-Original-To: caml-list@yquem.inria.fr
Delivered-To: caml-list@yquem.inria.fr
Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104])
	by yquem.inria.fr (Postfix) with ESMTP id 3299DBBAF
	for <caml-list@yquem.inria.fr>; Mon, 17 May 2010 21:21:54 +0200 (CEST)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AikCAPsz8UvUTWUIe2dsb2JhbACDGIJimAAVAQEWIgQerH6QcYElbVCBRGoE
X-IronPort-AV: E=Sophos;i="4.53,248,1272837600"; 
   d="scan'208";a="50762470"
Received: from mx4.wp.pl ([212.77.101.8])
  by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 17 May 2010 21:21:53 +0200
Received: (wp-smtpd smtp.wp.pl 15413 invoked from network); 17 May 2010 21:21:50 +0200
Received: from pfpleia.if.uj.edu.pl (HELO [149.156.90.26]) (d0@[149.156.90.26])
          (envelope-sender <d0@wp.pl>)
          by smtp.wp.pl (WP-SMTPD) with AES256-SHA encrypted SMTP
          for <caml-list@yquem.inria.fr>; 17 May 2010 21:21:50 +0200
Message-ID: <4BF196F3.5050508@wp.pl>
Date: Mon, 17 May 2010 21:20:19 +0200
From: Dawid Toton <d0@wp.pl>
User-Agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.1.9) Gecko/20100423 Thunderbird/3.0.4
MIME-Version: 1.0
To: caml-list <caml-list@yquem.inria.fr>
Subject: Binding and evaluation order in module/type/value languages
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
X-WP-AV: skaner antywirusowy poczty Wirtualnej Polski S. A.
X-WP-SPAM: NO 0000000 [kZNk]                               
X-Spam: no; 0.00; ocaml:01 memoized:01 compiler:01 sig:01 struct:01 struct:01 rhs:01 rhs:01 memoization:01 equality:01 equality:01 assert:01 assert:01 int:01 int:01 

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#