[e-lang] Membranes in Emily?

[Paul Snively]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

David Hopwood wrote:

> Mark S. Miller wrote:
> > At
> > http://lambda-the-ultimate.org/node/1625#comment-19906
> > an interesting thread has started up, trying to express the  
> membrane pattern
> > in strongly typed languages like O'Caml and Emily.
>
> My opinion is that it probably needs a Dynamic type, for example as  
> supported
> by Acute or Alice ML.
>
This would certainly do, but would be overkill. :-)
> (Some of the posts on LtU suggest that you need dependent types;  
> that's
> overkill. So is doing a global transformation using camlp4 or  
> MetaOCaml.)
>
I'm the one who proposed both dependent types and camlp4/MetaOCaml as  
possible solutions to the problem, and you're right; they're also  
overkill. It turns out that type-indexed functions are enough to do  
the job; the sub-thread around a simple solution in Standard ML can  
be found at <http://lambda-the-ultimate.org/node/1625#comment-20016>.

> Since you also need a Dynamic type to fix the hole in OCaml's type
> system (http://c2.com/cgi/wiki?OcamlTypeSafetyProblem) without losing
> functionality, I think this is definitely the way to go.

It isn't actually the case that you need a full Dynamic type to have  
type-safe marshalling; please see, for example, Peter Sewell's work  
on <http://www.cl.cam.ac.uk/~pes20/hashcaml/> and <http:// 
www.cl.cam.ac.uk/~pes20/acute/> as well as <http://www.pps.jussieu.fr/ 
~henry/marshal/>.

There's an excellent paper, "Encoding Types in ML-like Languages," at  
<http://www.brics.dk/RS/98/9/BRICS-RS-98-9.pdf>. While the whole  
paper is worth reading, Section 5, "Related Work," contains  
discussions of the Dynamic type, Intensional type analysis, and  
Haskell type classes. The subsection on the Dynamic type also  
discusses staged programming. Of course, type-indexed functions arise  
in the discussion of dependent types, and so I feel somewhat  
vindicated that my intuitions about dependent types and/or  
metaprogramming approaches were not entirely off base, but am happy  
to see that mechanisms exist, given nothing more than Hindley-Milner  
type inference, that support the provision of something functionally  
equivalent to the membrane pattern. Having said that, much work  
remains to be done to make the application of the pattern in Standard  
ML, O'Caml, Haskell... as syntactically painless as humanly possible.

Best regards,
Paul
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.3 (Darwin)

iEYEARECAAYFAkTILfgACgkQS6yIxITC5OpOjwCgv1Q8Rb17hhhaWs6VOteqn6AO
QtMAoJJm9uA8iiHzTDvA4LcvR7QccK+D
=7bT7
-----END PGP SIGNATURE-----