Lambda the Ultimate

This paper seems to be a fleshing out of the new work he discusses in this talk; I'm sure he's given it elsewhere too.

What is a "homogeneous, pure static type system"?

What I intend by this is the "ordinary" kinds of static type systems we usually talk about that are uniform and closed over the "whole system" of a program.

Perhaps it is easier to understand what I mean by looking at examples that don't fit this label.

The system in the Wadler paper allows stronger local guarantees to coexist with weaker global guarantees (or vice versa). In this sense, it is not homogeneous across the system that it constructs.

It is also not purely static, since it also has a distinct dynamic component.

Another example can be seen in Andreas Rossberg's thesis in relation to Alice ML pickling, where to support distributed systems each module is statically typed, but there is dynamic component to type checking to support distributed modules.

A more ambitious counter-example that I have yet to see, and which I have been thinking about in terms of Tim Sweeney's desiderata for a new language, would allow different modules to have different type systems entirely.

Let's say you could use a dependent type system on modules you were comfortable/able to have be "total" in the "necessarily terminating" sense, whereas you could use a less rich type system on a module that absolutely, positively required general recursion, i.e. potential non-termination.

An extension of what Wadler is proposing might allow for you to maintain what guarantees are portable across modules, but still allowing stronger guarantees where you really want and can afford them.

The blame game allows this to remain useful across the module boundaries.

it's unfortunate to give a function a type like forall a . a -> a if it actually fails a runtime typecheck unless you pass in a boolean!

Perhaps this is a case where the direction of the cast needs to be restricted: if a function of type forall a . a -> a is defined in a different module I can safely cast it to a boolean -> boolean in my current module with no risk and to a Dyn -> Dyn with only "blame" risk.

Obviously, though, we need more work to make such systems play well together sensibly.

I'm optimistic about the modal approach to giving strongly-normalizing dependently typed languages Turing-complete sub-languages

I agree this is an interesting approach, but I'm not sure in what way you think it is fundamentally different from the kind of system that Wadler is proposing. In both cases, to my way of thinking, there is a mixture of systems with a "blame boundary".

Perhaps this is a case where the direction of the cast needs to be restricted: if a function of type forall a . a -> a is defined in a different module I can safely cast it to a boolean -> boolean in my current module with no risk and to a Dyn -> Dyn with only "blame" risk.

Instantiating a polymorphic function at a more specific type is not a cast, and cannot fail. I'm not worried about packaging up and passing around completely statically typed polymorphic functions (Clean dynamic's seems to handle it fine). I'm worried about what happens if the implementation of a polymorphic function contains untyped code.

Say I'm writing a polymorphic identity function and I just can't get the job done without the freedom and rapid development advantages of some untyped code. There's a problem here for the implementation strategy - usually parametric polymorphism is handled by type erasure, but if I need to box up my argument as a Dyn to pass to the untyped world I need to know what tag to use, so at least some polymorphic functions seem to need an actual argument for some of their types. There are also some problems for the programmer, or maybe just one big problem. A polymorphic type signature is a promise that the function is going to work for any sort of arguments, but it seems like the untyped code could assume any specific type it likes, obviously without the type system noticing. More generally, all the free theorems die. Hmm, I wonder if you can fix both by using parametricity contracts in the untyped world?

I'm optimistic about the modal approach to giving strongly-normalizing dependently typed languages Turing-complete sub-languages

I agree this is an interesting approach, but I'm not sure in what way you think it is fundamentally different from the kind of system that Wadler is proposing. In both cases, to my way of thinking, there is a mixture of systems with a "blame boundary".

I both of these systems might possible have a place in the same language, but I don't see how they are similar. The partiality monad stuff is very much one-sided, it allows some interaction between strongly normalizing and potentially nonterminating code, mostly just nonterminating code using strongly-normalizing functions, but the point is to know that certain expressions (the types) can't contain or depend on any potentially non-terminating expressions, so you don't actually have to execute them to preserve logical soundness. Something similar could be useful in these mixed type systems, some kind of deeper cast operation you could apply to dynamic values that would completely walk the data structure or value and promise you wouldn't get any dynamic type errors later on. (See also undoing dynamic typing, but that uses continuations to jump back to the coercion when the cast fails, not so useful after you've already launched the missiles).

Instantiating a polymorphic function at a more specific type is not a cast, and cannot fail.

Of course. The subtle difference is where something that is a polymorphic function on one side of the boundary is only visible on the other as some of its instantiations.

This is the conceptual readjustment I'm talking about here: to stop thinking about it as "the" type system, and to think about it instead as localized type systems with interaction boundaries.

both of these systems might possible have a place in the same language, but I don't see how they are similar.

The similarity is conceptual rather than in the details. In some ways, I would argue that monads are already one technique to allow two different type systems to interoperate across a safety boundary.

Where my thoughts have been going lately are in the direction of a CTM hierarchy for type systems: use the strongest type system (analogous to less state) you can when you can, and only use weaker type systems as your problem requires it.

(This interrelationship between type systems and degrees of statefulness I think is a deep one, though at this point more notional than rigorous.)

Obviously to allow this kind of mixing to occur, a lot of work needs to be done at the borders to make sure it all makes sense in the end. Which is why I find this paper and others like it (e.g. the parametricity contracts one you mention) so interesting.

Broken link. Fixed.