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

[Sandro Magi]

Jonathan S. Shapiro wrote:
> Modern, statically typed, safe programming languages universally include
> dynamic typing in a limited way. The problem is unions, and the need to
> ensure that the union tag field has been properly checked when code
> operates on that union leg. ML, Haskell, BitC, and so forth all perform
> checks of this sort.

Indeed, algebraic types can be used as a more disciplined form of
"dynamic typing", where "casting" is deconstructing the type via pattern
matching, and where matching is forced to be exhaustive.

> Finally, a side comment on the whole static/dynamic issue. There are
> real restrictions that a safe static type system imposes. One, which
> MarkM can explain better than I, is that static types and first-class
> messages are not really compatible (more precisely: first class reply
> messages) within the current state of the art of type theory.

What are first-class reply messages? If you mean replying to a different
agent from the caller, then this is continuation passing style. I
suspect there's more to this though. There is a substructural type
system for delimited continuations [3], which are known to be one of the
most general forms of effects; any effect can thus be expressed in terms
of delimited continuations.

> In practice, however, I have not found any of these limitations to be
> compelling practical problems. This leads me to the opinion that the
> static/dynamic "battle" is *usually* a battle about something else
> entirely: the cost of annotating a program with types. And it is less
> about the cost of annotation per se than it is about the cost of being
> required to annotate before appropriate types are properly known (e.g.
> in early prototyping).

But as you say, algebraic types are statically checked dynamic types, so
prototyping shouldn't be much more onerous.

> Once they get over the new user hump, ML and
> Haskell users do not seem to incur much prototyping overhead in
> comparison to users of more dynamically typed languages.

I've always suspected that it's more about the initial titanic battles
getting your program to pass the compiler's analyses. Consider
dynamically typed languages: the runtime errors reported are directly
related to the operational semantics of the language which the developer
holds in his head.

Contrast this with a sophisticated type system which can produce cryptic
error messages during unification; the developer must interpret the
error messages according to how the types are interpreted, then map that
to the operational semantics of the language. This is particularly
damning for a newbie; coming from the C/Java tradition, I remember my
struggles first learning OCaml.

Polymorphic variants are a particularly bad example where 100+ page
errors are not unheard of. Cryptic errors are a known problem, and there
has been work on improving them [2]. The situation is definitely better now.

> The first class message issue is arguably quite real, but it occurs at
> exactly the place where the runtime meets the language, and I/O is
> inherently a place where static typing breaks down at the boundary in
> all languages.

First-class messages are subsumed by first-class labels for which a type
system exists. Perhaps the first-class reply messages are a different
issue though?

Sandro

[1] http://lambda-the-ultimate.org/node/174
[2] Helium is a friendlier subset of Haskell focusing on teaching with
very precise errors: http://www.cs.uu.nl/helium/
[3] http://okmij.org/ftp/Computation/Continuations.html#delimcc-type