From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id JAA01645 for caml-red; Wed, 10 Jan 2001 09:21:08 +0100 (MET)
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id PAA11831 for <caml-list@pauillac.inria.fr>; Tue, 9 Jan 2001 15:59:19 +0100 (MET)
Received: from mail5.microsoft.com (mail5.microsoft.com [131.107.3.121])
	by concorde.inria.fr (8.11.1/8.10.0) with SMTP id f09ExHP11054
	for <caml-list@inria.fr>; Tue, 9 Jan 2001 15:59:18 +0100 (MET)
Received: from 157.54.9.108 by mail5.microsoft.com (InterScan E-Mail VirusWall NT); Tue, 09 Jan 2001 05:36:59 -0800 (Pacific Standard Time)
Received: by inet-imc-05.redmond.corp.microsoft.com with Internet Mail Service (5.5.2651.58)
	id <CS320KG8>; Tue, 9 Jan 2001 05:36:57 -0800
Message-ID: <112C6E8A1B25D34BB27D48D2FD2E96CFC9DECE@TVP-MSG-02.europe.corp.microsoft.com>
From: Claudio Russo <crusso@microsoft.com>
To: Frank Atanassow <franka@cs.uu.nl>
Cc: caml-list@inria.fr
Subject: RE: first class modules (was: alternative module systems)
Date: Tue, 9 Jan 2001 05:36:17 -0800 
X-Mailer: Internet Mail Service (5.5.2651.58)
content-class: urn:content-classes:message
Sender: weis@pauillac.inria.fr

Hi Frank,

This should do it...

signature S = sig type t; val x: t; val y: t -> int end;
functor F A:sig val b: bool end = struct 
  structure X as S = if A.b 
     then [structure struct type t = int; 
                      val x = 0; 
		          val y = fn x:t => x
                     end as S]
     else [structure struct type t = int -> int; 
                      val x = fn x:int => x;  
	                val y = fn f:t => f 1  
                     end as S]
end; (* X.t depends on the value of A.b *)
structure Y = F(struct val b = true end); 
structure Z = F(struct val b = false end); 
(* if functors are applicative then Y.X.t = Z.X.t *)
val z = Z.X.y (Y.X.x)  (* applies 0 to 1, a run-time error *)

Note that the definition of z  goes "wrong" if F is applicative (a la
O'Caml, and expressible in Mosml syntax by omitting the parenthesis
around A:sig ... end), 
but is ill-typed if F is generative (as in Standard ML). The program is
rejected by the (crude)
syntactic restriction that functor bodies can't eliminate first-class
modules, 
except within inner Core let expressions.

Section 7.4 of my thesis discusses this issue in detail. Xavier's paper
on applicative functors has a similar example. The example above appears
in my forthcoming Nordic Journal of Computation article.

Cheers,

Claudio

> -----Original Message-----
> From: Frank Atanassow [mailto:franka@cs.uu.nl]
> Sent: 09 January 2001 12:31
> To: Claudio Russo
> Subject: Re: first class modules (was: alternative module systems)
> 
> 
> Hello,
> 
> Claudio Russo wrote (on 08-01-01 07:11 -0800):
> > This is actually more general (and convenient) than the 
> open construct
> > because it lets you open first-class modules  at top-level 
> and within
> > structure bodies, not just within Core expressions. If functors are
> > always generative, this is ok, but it interacts badly  with 
> applicative
> > functors (programs can go "wrong"). 
> 
> I have seen you allude to this type soundness issue several 
> times now. Can you
> give an example of a bad program which violates your 
> condition?  (Or just
> point me to the place in your thesis or a paper where it is 
> elucidated.)
> 
> -- 
> Frank Atanassow, Information & Computing Sciences, Utrecht University
> Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands
> Tel +31 (030) 253-3261 Fax +31 (030) 251-379
>