RE: first class modules (was: alternative module systems)

[Claudio Russo <crusso@microsoft.com>]

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
>