Lambda the Ultimate

Anton writes:

But the question of whether latent types are actually "types" is a quibble - to have this discussion, about types in DT languages, we need to talk about something more specific than just "program properties". We'd have to talk about e.g. "type-like program properties", which, with appropriate definitions, can become types.

A similar view was championed by Patrick Cousot in his 1997 POPL invited paper, Types as Abstract Interpretations. He starts with a standard semantics of the untyped lambda-calculus, and then designs Curry-style type systems (including familiar rule-based presentations) using abstract interpretation.

The teaser is from Section 14:

The question "What is a type system" has hardly received a formal answer. Type systems can be viewed as abstract semantics in the lattice of abstract interpretations which are more abstract than a type collecting semantics which is the most general type system in that it is more precise than the reduced product of all existing type systems.

The paper is quite dense, and the reader is expected to have some prior knowledge of abstract interpretation.

Nice reference, thanks, although I'm going to need to take a few months off to get through it. IIRC, Paul Snively made some reference to this sort of work -- the idea of a DT to ST slider based on partial evaluation -- in one of the earlier incarnations of this thread. Perhaps Frank would be happier if I expressed my point of view in terms of abstract interpretation. In fact, I did that to some extent in this LL1 post last year.

This post looks relevant (look for "continuum").

Also, I think that in twenty years there will no longer be any debate about static vs. dynamic typing, and that instead most languages will instead provide a smooth continuum between the two, as people realize that there is no fundamental dichotomy there. Also languages will have more than one level of types: the types themselves will have types, and so on. But we will be able to treat types in a similar way to the way in which we treat values: we will be doing computations with them.

I wonder if one of the "levels of types" in this picture might be latent types? ;o)

Another comment of Frank's which is right in line with what I think is "I have a feeling that DT languages are not at the 'end of the line' and could go further by adopting online partial evaluation techniques".

I completely agree with both Frank's quote and Anton's response to it. Let me see if I can also find the old thread about how such a "tower of types" might look, with Tim Sweeney and Frank ping-ponging. Ah, here it is. I guess it's no secret that I'm basically following Tim's lead here, having read the Ontic paper and found it just as compelling as Tim did. That's not to say that Frank's line of reasoning lacks merit, but rather that I'm not competent enough in the requisite theory to see the value in a non-set-based approach to the subject. But it's worth noting that both approaches seem to result in a kind of "tower of types" that one can construct terms around, and if these types are first-class and can even be defined/checked at runtime and we wish to call these "latent types," I find nothing wrong with that.

Heck, I don't even have anything against latent types as they're defined today. I only have a problem with claims that static types can't do things that they have been demonstrated to do, or that latent type systems somehow represent a proper superset of static type systems. That's all. Maybe if I posted more about some of Oleg's Scheme stuff people would believe me. :-)

...because interpreting types as sets of values breaks down badly in the presence of polymorphism. Informally. the reason is that if you interpret a type as a set, quantifying over a polymorphic type means that you are quantifying over the class of all sets, and that is "too big" -- you can do Russell's paradox-style tricks.

Tim Sweeney posted a while back on that very subject. In the context of Ontic, there's apparently an interplay of the notion of types as sets of potential values, along with some other constraints on its semantics, that prevent the collision with Russell's paradox and its ilk.

...do things like interpret types as domains. But whatever you do, it's no longer the case that the element of a set is a value, and you can't use ordinary set-theoretic to reason about types. It just seems cleaner to me to bite the bullet and adopt a categorical semantics, and treat any pointwise reasoning you have to do as operations in the internal language of whatever categorical thing you're using.

and if these types are first-class and can even be defined/checked at runtime and we wish to call these "latent types," I find nothing wrong with that.

I'm not sure if we're using the term "latent types" in the same sense. I've been using it in the context of "syntactic" type theory, as defined by e.g. Pierce in TAPL. In that context, types are syntactic, and apply to program terms. The things you can test at runtime are tags, related to but not to be confused with types (because they're not completely isomorphic to each other). Latent types aren't first class, even if the language has some first-class representation of its tags (and note that e.g. standard Scheme has neither first-class types or tags, although it supports runtime checking of tags).

The difference between a latently- and a statically-typed program from this perspective is that the statically-typed program has a fully formally-defined type scheme. The latently typed program does not have a formally defined type scheme. It may have a partially-specified type scheme, perhaps specified in comments, as is common in Scheme and Erlang. But even if its types are never written down, programmers still rely on implicit, static, type-like information in order to be able to write code - it's how they know that an object referred to by a particular variable will accept a particular message, for example.

Programmer in dynamically-typed languages tend to think about types in first-class terms, as runtime properties of values, but in Piercian terms, those runtime properties are tags, and those programmers are still in fact reasoning about types when they write e.g. "x.foo()", knowing statically that the values that flow through x at runtime will accept the 'foo' message.

Part of the reason I was focusing on this back when we were having this discussion is that many people on both the static and dynamic sides seem not to appreciate that both sides deal with the same kind of static type-like information. I started these threads by responding to Luke Gorrie's question about why type systems are interesting, and my point was that even the most dynamically-typed programs contain this latent, static type-like information, and that we depend on it for reasoning about code.

In fact, even statically-typed languages may contain latent type information. In OCaml, if you make use of structural subtyping by using a set of common methods across multiple unrelated classes, you've effectively created a latent interface or type, just as you might do in Smalltalk or some other dynamically-typed language. In a Haskell program, you would be forced to encode this kind of latent information in the type system, e.g. in the form of a typeclass.

Similarly, if you use a data type for tagged values, like Univ, to encode a latently-typed program in a statically-typed language, the nature of the latent type information doesn't change - it remains latent. Again, we have a situation in which an apparently statically-typed program has latent type information - potentially lots of it. This implies that programmers in statically-typed languages should be aware of latent types, although in their case, their response to it may often be to attempt to encode it fully the type system, so that it is no longer latent.

I only have a problem with claims that static types can't do things that they have been demonstrated to do, or that latent type systems somehow represent a proper superset of static type systems.

In the sense I'm using the term, I certainly claim that latent type systems are an informal superset of static type systems. Static type systems can be seen as "merely" particular formalizations of a much larger class of less well-defined latent type systems. Being informal, this relationship may not qualify as a "proper" superset, though.

I just wanted to follow up extremely briefly to let you all know that I still need to read this paper. I skimmed it very briefly the day it was posted, and noted the bullet points, which basically say that typed reflection is both necessary and possible. I found that very heartening and look forward to reading the full paper.

Simple matching will fail to prove compatibility of types if it is too simple. For example imagine that I am trying to do this:

void foo(int : [1,...] y);
...
int : [5,6,7] x = 5;
foo (x);

Textual matching would fail to detect that {5,6,7} is a subset of the positive integers, and hence that x can be passed as the argument of foo. This is why type systems are not trivial.

I think textual matching is enough, if the following substitutions exist:

5 => positive 5
6 => positive 6
7 => positive 7

Suppose that our function is:

void foo(positive n);

Then the following is valid:

foo(5);
foo(6);
foo(7);

because '5', '6', '7' can be substituted by 'positive 5', 'positive 6', 'positive 7' respectively.

The system above could be generalized with any symbol. Let's suppose we have variables, instead of numbers:

let unsigned n1 = 5;
let unsigned n2 = 6;
let unsigned n3 = 7;

with the following substitutions:

unsigned N => positive N

by simple textual matching, we have the following substitutions:

unsigned n1 => positive n1
unsigned n2 => positive n2
unsigned n3 => positive n3

Therefore the variables n1, n2 and n3 can be used in any context that a positive number is required.

To have an extensible type system based on such substitutions you would have to allow users to add their own substitutions. Now, you have to make decision about what substitution rules you allow, and whether or not you want to constrain that so that so that type checking can be proven to terminate.

Doesn't Ada already allow constraints to be applied via subtyping? I'd imagine that provides a fairly good existence proof that "a complicated theorem prover" is not required.

I read on the same page that

conversion is checked at runtime

so it's not purely static.

To be honest, I know little or nothing about Ada (Ehud? can you help here?). However, my impression is that the runtime checks are carried out only in the case of converting between different Types, but not in the case of different Subtypes of the same Type (i.e. constrained version of some larger Type).