[cap-talk] David Wagner's Google techtalk is now up!

Sandro Magi smagi at higherlogics.com
Wed Dec 12 22:39:34 EST 2007


Mark Miller wrote:
>> Mark Miller wrote:
>>> A dynamic type system can provide exactly as much integrity (safety,
>>> consistency) as a static type system. In both cases, integrity
>>> violations are prevented -- whether statically or at runtime.
>> What definition of safety are you using?
> 
> Consistency is preserved.

I was a little confused about "consistency", but found the reference in
your thesis, Section 5.6. A brief glossary of general security terms [2]
on the wiki.erights.org might be handy; Norm's current list [1] is
lacking these terms.

Back on the consistency issue, it strikes me that this is only a useful
property for shared mutable state; after all, a purely functional data
structure is naturally defensively consistent up to resource exhaustion.

So I agree that a purely functional dynamically typed language's
consistency properties can match a purely functional statically typed
language's. But no language can do without shared state (ie. I/O) at
some level.

So the real question is whether static typing can be exploited to ensure
consistency in the presence of effects. As you say, simple type systems
don't help you much as they are currently used, but reifying effects as
data, as in monads, help reasoning about effects using even simple
types. Such patterns are just very cumbersome in simpler type systems.

There is a great opportunity here for richer type systems too; type and
effect systems seem particularly poised to help here as they directly
represent effects in the type system.

Sandro

[1] http://www.cap-lore.com/CapTheory/Glossary.html
[2] safety, consistency, robustness, security; any other general terms
bandied about?


More information about the cap-talk mailing list