From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 9D49FBBAF for ; Tue, 18 May 2010 05:33:24 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApwEAIan8UuFBoIF/2dsb2JhbACDGJtTqk4BgkOOTAEEgSKBQIFBbYNC X-IronPort-AV: E=Sophos;i="4.53,252,1272837600"; d="scan'208";a="51342437" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail2-smtp-roc.national.inria.fr with ESMTP; 18 May 2010 05:33:23 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id EBA85B685; Tue, 18 May 2010 12:33:20 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (camel-172 [172.16.254.4]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id ACFD288A8; Tue, 18 May 2010 12:33:20 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= date:message-id:to:cc:subject:from:in-reply-to:references :mime-version:content-type:content-transfer-encoding; s=alpha; bh=fZJ0uq+5yGJtb3z+gfYyvZJtJJc=; b=pEgN3gdTek+LmwXB8bItBXt+vWEh JB+SuSVhjD98CLC5hFJSpqNoYbYAfOkg7goDqnpsbZUK5MIuq+KStd6j23SPq2Q4 VpVB728HbJdYX1lDLDOGzBIChKi9uOgiwUV/J8TxE/OoybCtFceLfwrWQB/H/Z9M eM6OwSvvohjvwhw= DomainKey-Signature: a=rsa-sha1; h=Received:Date:Message-Id:To:Cc:Subject:From:In-Reply-To:References:X-Mailer:Mime-Version:Content-Type:Content-Transfer-Encoding; b=UV9S9eAWGx+UIOa2IkD6VHu1ovbVw8I/W7tdDjpjsgZHULodOaSo5fMN1m1+uahaJnEuEJYUolVPlVlpqOLfVHQocbbTlrfpgD4xHnDqm5Hjgjhvhl3U8fow/jpK/lZ0K29drM5uBr8H8VVaIbLDrgGYW/uUomSVNifmSBHYioI=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from localhost (bsdserver02 [172.16.249.2]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 8437C8894; Tue, 18 May 2010 12:33:20 +0900 (JST) Date: Tue, 18 May 2010 12:33:13 +0900 (JST) Message-Id: <20100518.123313.173589671.garrigue@math.nagoya-u.ac.jp> To: d0@wp.pl Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Binding and evaluation order in module/type/value languages From: Jacques Garrigue In-Reply-To: <4BF196F3.5050508@wp.pl> References: <4BF196F3.5050508@wp.pl> X-Mailer: Mew version 6.3 on Emacs 22.3 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=iso-2022-jp Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; ocaml:01 memoized:01 compiler:01 semantics:01 ocaml:01 sig:01 struct:01 struct:01 rhs:01 functors:01 applicative:01 rhs:01 memoization:01 memoization:01 haskell:01 From: 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. 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 = 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