Lambda the Ultimate

Suppose we have an untyped programming language, and then impose a type discipline on it. So, now we will reject certain programs as being ill-typed, for whatever reasons the type system designer had in mind. That's clear, but now ask, what else happens?

Well, a surprising fact is that the imposition of a type discipline changes the language's natural notion of program equivalence. Intuitively, two program modules are "contextually equivalent" when all client programs that could use them ("contexts" in PL jargon) have equivalent behavior when you switch between the module implementations.

Why? This is because client contexts are themselves programs, and so there are fewer contexts in the typed world than the untyped. This is the underlying mechanism that makes type abstraction work: we use the type discipline to ensure that there are no client programs that can "peek under the covers".

As an example, consider the following ML program:

module type EVEN =
sig
   type even

   inject  : int -> even option
   outject : even -> int
end

module Even : EVEN = 
sig 
   type even = int
  
   let inject n = if n mod 2 = 0 then Some n else None
   let outject n = n     
end

Because the type Even.even is held abstract, we know with certainty that whenever v is a value of type Even.even, then calls of the form (Even.outject v) mod 2 will always return 0.

Is this the kind of thing you were asking about?

First, your recollection is correct: static typing is necessarily conservative over execution because the entirety of the dynamic semantics of the program is not available at compile time except in a handful of extreme, trivial cases. This is the chief critique of static typing from dynamic typing aficionados that has any "bite," in my opinion, although in practice I find the observation trivial. If you have a Turing-complete dependent type system, the ε between what you can express at compile time and what you can't becomes infinitesimally small, and even short of that you can get vastly more helpful static guarantees out of, e.g. GADTs in Haskell or Scala, modules and phantom types in ML, etc. than most people are aware of.

It's precisely in this context—the context of relatively rich type systems like those of OCaml, Haskell, Scala, etc.—that we find the beginning of the answer to the latter part of your question. It's one thing to say "I have static typing with type inference, so I don't have to spell everything out but the compiler keeps me from making boneheaded mistakes," and here I think dynamic typing aficionados are essentially correct in saying "big deal; I get that much out of my unit tests," assuming good test coverage. An important line gets crossed, though, in making the transition to "typeful programming," where you, the programmer, express important program invariants using the type system, so that your program will not compile if you should happen to violate one or more of those invariants. Using types to implement proper units in numerical code is indeed an excellent example of this. This thread goes more deeply into the idea of sealing off important invariants in a module and having the type system then guarantee that these invariants hold throughout the program.

I may be misunderstanding the questions, but it almost sounds like benckla is asking about research into what I'll call "domain specific type systems." I.e. most type systems that are researched give you some fairly general concepts for preventing a fairly broad range of problems and leave it up to a programmer to map their domain into the type system. But just as languages can be targeted to domains, are there DSLs with type systems optimized for fairly specific areas? An example might be a physics based DSL with a static type system that natively understands units so it can statically prevent adding centimeters to ergs without forcing the developer to figure out how to make it all hang together.

To answer the question broadly, I think most PLT research into type systems is naturally going to be more general in nature but such research may often be motivated by such specific problems. So expect that while there are going to be DSLs with type system optimized for their domain, it's unlikely that you'll find much core research into the subject of designing such systems. That does seem to fall more on the SE side of the world rather than the PLT side.

Benjamin Pierce gave a talk (discussed here) that sounds like it relates closely to your distinction between imposed versus enabled by a language.

I am a bit baffled and I am perhaps simply again not understanding what it is you are after. Do you have any experience programming in Haskell or, alternatively, Ada? If so, have you also read examples of good code in these languages, or style manuals or textbooks? It seems to me that one of the main things that are emphasized is how to use the expressive type systems (imperfect as they are) to encode domain and program specific invariants, in order to assist design, programming, debugging, reuse etc. etc. At least that's what I tried to show students when I taught software engineering with Ada.

Or am I missing the point entirely?

P.S

Here is an ancient riddle I posed students that is a short illustration of what I have in mind.

Thanks Ehud, I think you do "get" what I am talking about except for one little twist: my original question was not "where can I find discussions of typeful programming," it was more like "where can I find discussions of typeful programming *in PL theory*, or are such discussions only to be found in software engineering?"

Here's yet another way of putting my question. "It seems to me that PL theory focuses on type systems with respect to where they draw the lines in the classic quadrants of any test: false positives, etc. What about what a type system enables within the "true positive" quadrant? Is that just software engineering? Or am I just ignorant of its discussions in PL theory?

...but my $.02 here is that it's difficult to talk about this from a perspective that is simultaneously PLT-based (that is, giving a detailed description of language and type system design properties that lend themselves to typeful programming) and pragmatic (that is, making the connection to solving specific problems, e.g. statically disallowing write operations to read-only files, or statically disallowing any access at all to a file that isn't open [in the first place|anymore]). I continue to claim that the most accessible such writing is that of Oleg Kiselyov and Chung-chieh Shan on Lightweight static capabilities, which are all about selecting domain-specific (pragmatic, non-PLT-founded) invariants, hiding them behind an inviolable abstraction barrier (PLT/type theory/module system), and extending their guarantees to the rest of the code. It's partly to make a point about what can be done even with the type and module systems we have today, but also to demonstrate why you might want an even more powerful type system, e.g. with explicit support for dependent types. Well worth gaining mastery of, IMHO.

OK then ;-)

There are all kinds of projects that explicitly attempt to make type systems more expressive (Paul is our resident expert on those). I'd mention a more general issue: the goal you are after is part of the context and background of the research. It is why a type system (or a type system feature) is being designed, proposed or analyzed. But most papers are not about the intuitive design process but rather on the provable properties of the resulting system. So when you read the papers you need to look for the motivation, come to seminars and conferences, or ask people in the community about why the type systems are of interest for expressing application-level invariants. These elements are usually not discussed at length in papers (be on the lookout for the "related work" and "further research" sections which often provide important clues...)