[e-lang] A broken brand?

Sandro Magi naasking at higherlogics.com
Thu Mar 6 09:40:27 EST 2008

David Wagner wrote:
> Sandro writes:
>> Unless I'm mistaken, this is a problem for sealers, which have many uses 
>> that cross machine boundaries.
> I'm ignorant about distributed systems, so perhaps I'm talking
> nonsense, but I don't quite follow this comment yet.  In a distributed
> system, transparent forwarders/proxies have to be implemented as part
> of the TCB (not at the application layer), and they have to have the
> ability to "forge" types (i.e., to pretend to be of any desired type).
> So I don't see why type-checking would prevent using these objects in
> a distributed system.

We have a disagreement on the fundamental assumption: I don't accept 
transparent interposition/forwarders are necessary, or even desirable. 
It sees significant use in object-oriented systems, but not much use in 
functional programming. By adding transparent forwarding, you lose 
"sitedness" properties, which I think are important for reasoning about 
local vs. remote systems.

See for instance "fswebtoolkit" [1], which distinguishes client and 
server computations using the monads in F# (called 'computation 
expressions'). Client computations are compiled to Javascript for the 
browser, while server computations execute server-side in the .NET VM. 
This site distinction is enforced at compile-time, so the compiler 
ensures that server and client computations cannot be mixed in the same 
expression, except via message sends. I think there's a great deal of 
value here, which interferes with properties provided by transparent 


[1] http://tomasp.net/fswebtools/files/*fswebtoolkit*-ml.pdf

More information about the e-lang mailing list