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

[Jonathan S. Shapiro]

On Thu, 2007-12-13 at 14:36 -0500, Sandro Magi wrote:
> Jonathan S. Shapiro wrote:

> 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.

I don't know anything about substructural type systems. The issue here
is that the output (reply) message type of the "send" primitive is a
function of the input message type, but this type relationship is very
hard to capture in any static way. For reasons I can no longer remember,
it is not (quite) something that dependent types can do. MarkM can
probably reconstruct what the issue was.

> > 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.

I think there is another factor as well, and it relates to the nature of
functional languages. In learning functional languages, we are led to
focus on defining functions, and we become frustrated when that does not
behave as expected (even when our expectations are wrong). In reality,
most of our prototyping problems are driven by data definition, and the
operations are more often consequences of the data structures. I think
what I am saying is that there seems to be an impedance mismatch between
the way we teach this class of language and the problems that real
programmers are trying to solve as they prototype. It is not clear to me
whether this is a result of some fundamental impedance mismatch between
these languages and real problems (e.g. lack of state) or if this is
merely a consequence of a demented pedagogy that sometimes seems to have
evolved its own perverse form of religious-style orthodoxy.

> 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.

It is clear that many compilers give particularly crappy error messages
where unification is concerned. This is something that Swaroop put a
bunch of work into in BitC. If you have a favorite simple example that
generates a crappy diagnostic, I'ld be interested to see if the current
BitC compiler does any better.

>  This is particularly
> damning for a newbie; coming from the C/Java tradition, I remember my
> struggles first learning OCaml.

Yes. It is very difficult to thread the OCaml through the ONeedle. :-)


shap