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

[Sandro Magi]

Jonathan S. Shapiro wrote:
> 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.

Ah, I thought it was something more complicated. As MarkM has just
pointed out, Paritosh's system for typing first-class messages would
work, as would any GADT-capable language. GADTs are a lightweight
dependent type.

Mark Miller wrote:
> Another part of the puzzle is highlighted by the incredible degree of
> difficulty that the static typing aficionados on LtU had expressing a
> statically typed membrane
> <http://lambda-the-ultimate.org/node/1625#comment-19906>. Although
> they did ultimately succeed, the difficulty they encountered and the
> obscurity of the result, to my mind, disqualified fully static type
> systems from being ready for practical use. If it's this hard doing a
> simple membrane, good luck doing Horton.

This is the complete solution:
http://lambda-the-ultimate.org/node/1625#comment-20065

I think the ultimate problem is that static languages and their
libraries are not built with access patterns and transparent
substitution in mind; they have a local-only mentality (and a
single-threaded mentality too unfortunately).

In type systems, objects provide encapsulation, and thus transparent
substitution, at the expense of strong binary methods (operations that
operate on two values of the same type). Abstract data types support
strong binary operations, at the expense of transparent substitution.
They are duals. Most strongly typed languages support the latter.

If I understand correctly, Vesa's solution reflects language values into
Membrane.t values which provides the necessary indirection for
transparent substitution (when combined with type inference). Dually,
statically typing binary methods for objects involves somehow exposing
the concrete type encapsulated within the object.

Vesa's solution, or something similar, should really be part of the
standard library of a statically typed functional language that supports
distribution, so some transparency for the user can be expected. Perhaps
AliceML has something to say here? It is a distributed ML after all:

http://www.ps.uni-sb.de/alice/

The ADT/object duality raises a question though: instead of trying to
shoehorn ADTs into a pattern more suited to objects, is there an
appropriate access pattern for ADTs?

Jonathan S. Shapiro wrote:
> 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.

Interesting you should say that, because when first approaching new
problems I find myself describing my data using ML data type definitions
(ie. describing the algebraic structure of the data), and the functions
almost always naturally fall out. I then translate the resulting code
into C#, which I'm forced to work with. ;-)

I think the data-first mentality works well in functional languages.

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

Can't think of anything off-hand, but I'll keep it in mind.

Sandro