Lambda the Ultimate

What's a good introduction to that solution to the expression problem in Haskell? I thought that type class dictionaries were a compile time affair? Edit: Oh sorry I didn't read what you said correctly, I thought you meant that you had one instance per datatype because you mentioned the connection to vtables, but you probably meant one instance per datatype-function pair (with one class per operation). In that case, I see how it's done and disregard this message.

Sounds like you have it right. "type A = B | C" becomes "type B;; type C", and every pattern matching function becomes a class, with each case of the match becoming an instance. You can see quite simply how this solves the expression problem, since arbitrary new types can be added with arbitrary cases and full static checking. Pattern matching reduces to dictionary dispatch, and this paper makes this transformation the canonical pattern matching technique.

Please see the encoding using extensible records of OCaml
http://okmij.org/ftp/tagless-final/course/final_dic.ml

In addition, tagless-final shows what seems to be the first solution to the extensible de-serialization, described at slide 18 of
http://userpages.uni-koblenz.de/~laemmel/TheEagle/resources/xproblem2.html
The solution is not perfect (duplication has a run-time cost), but at least it exists.

I have some questions about the last link "Spin-offs from the Expression Problem". The presentation starts by showing the problem that the types are too precise and therefore Haskell will not accept putting those expressions in a list. Existential types are identified as a non-solution from an extensibility standpoint. At the end a solution is presented where instead of lists nested pairs are used. How do you program with those kind of lists? My superficial understanding would say that to solve the problem with the too precise types, you've just pushed the problem into the lists. Aren't you going to need existentials again to use those lists?

Do you need to rewrite the whole Haskell library? How do you program in that style, in general?

The expression problem says that you should type check modularly. How do you know that you didn't put too much information in the types? As a degenerate case can imagine a type system where you just put ALL the information about a module into the types, effectively making type checking non-modular again by simulating the "solution" that delays type checking of a module until the module is used.

I should point out several ways of putting heterogeneous elements into ordinary lists (without using existentials). For example, we can use universals or build unions on the fly. These methods are summarized at
http://okmij.org/ftp/Computation/Existentials.html#type-unions

By the way, the tagless-final approach is different from the one shown on the slides; no heterogeneous lists are used and no type-level programming is required.

I'm not sure I understand your last question. A module may export data declarations, type classes and type functions, which may be faulty. Some faults like data type with no inhabitants sans bottom, type class with no members, type functions doing a wrong thing are discovered only when we try to type check the code using these data types, classes, functions. That is not much different from an error of forgetting to export a function from a module. This error will be caught only when you try to import that module and use the function.

I also don't understand the question about putting `too much information in types'. Too much for what? Haskell offers a programmer enough freedom to express desired static invariants in types -- that is, statically preclude some classes of undesired behavior. (The value of any time system is mainly not in what it allows, but in what it statically prevents. For example, if the GHC type checker agrees that an expression has the type Int, then the evaluation of that expression will never give you a string, for example.) It depends on the task at hand to determine which behavior is highly undesirable to warrant trying to preclude it statically (and balance that assurance against the cost of designing and using sometimes fancy types). Hindley-Milner type system offers the amazingly good balance, frequently under-appreciated. Haskell and OCaml offer many ways of weakening (variants, dynamics) and strengthening (phantom types) the assurances. (Of course languages like Agda and Coq shift the balance towards strong assurance by making the encoding of desired invariants much less convoluted).

Thanks for you explanation. I now also looked at the tagless-final approach, and it it very nice (and I'm still reading).

In PushNegFI.hs you pose a question:

-- Open research question: can the intermediate Exp data type be removed
-- by deforestation? Can we propose fusion laws to eliminate Exp?

Now I don't have an answer to this, but you can do arbitrary pattern matching on final terms without first converting them to initial terms. You don't even need to traverse more than you need to with the initial approach. Start with a pattern match, then unnest the patterns by converting it to nested case expressions where each case only pattern matches on constructors directly. Then for each such case expression build a dictionary that does that pattern match. For example:

foo (Lit a) = f a
foo (Neg (Lit a)) = g a
foo (Neg (Neg x)) = foo x

Unnests to:

foo (Lit a) = f a
foo (Neg x) = bar x

bar (Lit a) = g a
bar (Neg x) = foo x

Convert to final style (with explicit dictionary passing):

foo y = y {lit a = f a, neg x = bar x}
bar y = y {lit a = g a, neg x = foo x}

This even works for pattern matching on multiple arguments simultaneously. It would be interesting to see if this kind of nested pattern matching can be made extensible in a usable way (i.e. not by manually unnesting and defining a type class for each nested case expression).

Is that correct or did I miss something?

Indeed, I'm a big fan of the tagless-final approach! You can see immediately how to safely extend the type class for an EDSL with new constructors and new functions without changing existing code.

About the only "unsolved" problem for the approach is metacircularity/self-interpretation. I'd love to see a language with the let-polymorphism approach Jacques describes at that link baked into a language, thus allowing fully typed metacircularity.

Host language functions are then themselves interpreted in the type class that defines the language, and they can be reinterpreted in different ways (like a monadic metalanguage, where functions are usually interpreted in the Identity monad) simply by supplying a new instance of the class. You get a lot of power with this sort of metacircularity (code optimizations, mobile code, automatic parallelization transforms, etc.).

I've implemented something like that. The language has a special construct that allows you to wrap an interpreter around a subexpression. Sort of like monadic reify/reflect but for all language constructs instead of just let. There is some weirdness going as a consequence of that. For example functions are essentially represented as their AST, so you get something quite like early Lisps.

The nice thing is that you can add monadic effects as you say, and also things that aren't monadic like laziness and I think also lazy non determinism (which doesn't fit the monadic interface exactly as Oleg shows in his papers).

For monadic effects it's also nice that you don't have to write any monad transformers: you just stack the monadic interpretations.

I am concentrating on the type-level aspects. It is very tricky. For example, see Rendel, Ostermann and Hofer's Typed Self-Representation where they have to resort to kind:kind to make things work.

And yes, everything in the language has to become both directly interpretable and available as an AST. The fun part is to try to merge those two representations. Aaron Stump's Directly Reflective Meta-Programming had managed to do that, at least operationally. Giving that system some types (which is what I am trying to do with Aaron) is turning out to be astonishingly tricky.

I should also mention Jay and Palsberg's recent Typed Self-Interpretation by Pattern Matching as also being related. They get even closer than others, but by using a combinatory calculus rather than a lambda calculus. Also, they cheat just a little -- so that they do get a typed self-interpreter, but they do not really get a fully typed language... (see the paper for the details, it is really subtle, but the authors do not hide this hole, they discuss it appropriately).

Excellent references. I'm really interested in this subject, so I'm glad it's getting some attention. I imagine Jay's paper is a follow up to his original work on the SF calculus.

As for typing it, it's obviously much trickier than I've been thinking. I was assuming that you could reflect the "context with a hole" you mentioned on the original tagless thread, in a continuation-style program expression (like used to type printf in ML), and get the required polymorphism that way. It seems reasonable in my head at least, but obviously I haven't worked it all out.

I actually think Ur is currently the only "production quality" language that supports extensible records and first-class cases. Am I wrong?

I'm not sure I'd be willing to claim it is a "production quality" language, but Links has full support for extensible records and first-class cases. (Links has been used to write a variety of non-trivial web applications, so I think it is fair to say it isn't a "toy" language, even if it isn't a "production quality" language.)

OCaml is almost there with its objects and polymorphic variants. The key features missing from OCaml are negative presence information (the type system cannot capture the type of an open row that does not contain a particular label) and the ability to refine variant types during pattern matching.

Links also uses rows for effect-typing, similarly to Blume et al.'s follow-up paper on exception handlers as extensible cases.

Now that cases/dispatch and sums/messages are first-class, most of the patterns used in dynamic languages can be typed, ie. message forwarding and proxies. Most other patterns are built from these foundations. The only remaining component is "dynamics", ie. transforming untyped data into typed objects, like parsing, serialization, etc. There are typeful solutions for these problems.

What's left in dynamic languages that can't be expressed in this framework?

What's left is the ability to ignore types as long as you're not interested them, for example during exploratory programming (aka optional typing).

This isn't really hindered by types. I actually find types helpful while prototyping.

What's also left is the ability to modify programs in arbitrary ways at runtime (aka reflection).

But no one is interested in modifying programs in arbitrary ways at runtime, people are interested in modifying programs in meaningful ways at runtime. That's where types come in.

I don't think your argument is that good, but wish to help:

• Behavioral equivalence between types is a difficult research issue, and offsets one form of reuse for poor metrics in another area of reuse
• Many type systems require heavy syntax to parametrize modules, and some do not allow hidden state for the purposes of defining temporary "garbage" for the purposes of scaffolding
• Many type systems have type inference that is not compositional, and so there are awkward edges in which heuristics must be employed to either ensure that programs terminate or that all programs are well-typed.
• Type level computation introduces dependencies on the typing algorithm for performance, correctness, etc. Which is fine if you can formally prove correctness and guarantee bounds on program execution time, I suppose.
• There are unsolved problems in type systems which could potentially better inform language design using type systems, such as the open problem in Pure Type Systems known as the Barendregt–Geuvers–Klop conjecture. When exploring with a powerful language, it would be nice if that language wasn't a mish-mash of ad-hoc extensions and even nicer to know our questions make sense.

Arbitrary changes doesn't sound enlightening. To be fair, I used to think the phrase arbitrary was a very impressive argument.

Other people disagree with you and find other things more helpful. The ability to ignore types completely is seen by some as essential during exploratory programming. Many static type systems seem to make it impossible to ignore them.

I agree, many static type systems make it much more difficult than it need be. Ignoring types is not essential to exploratory programming, having a language that supports easy extension, composition and reasoning about abstractions is essential. Many typed languages make extension difficult in various ways. First-class cases + a system for dynamics eliminates most of these difficulties, thus my comment.

What changes at runtime are meaningful may be hard or impossible to anticipate. Therefore, depending on the situation, the more arbitrary changes can be made, the better.

This is not hindered by typing at all. Live upgrade simply requires runtime support. Whether your language is typed is irrelevant. It just so happens that typed languages thus far avoid relying overmuch on runtime support, but this is not strictly necessary (mainly because they erase types).

Dynamic languages, not being able to rely on a compiler producing well-typed code, must have significantly more runtime support so they provide these features by default.

As a final note, I recommend you hit the "reply" link when replying to comments so discussions are properly threaded.

Ignoring types is not essential to exploratory programming

You make the mistake to think that what is subjectively essential for you to be able to do exploratory programming must be essential for others as well. This is not the case. Exploratory programming is primarily creative work, and different people have different essential needs to be able to be creative. The ability to ignore types is considered essential by some, and just because this is not the case for you personally doesn't make that fact go away.

Live upgrade simply requires runtime support. Whether your language is typed is irrelevant.

There are cases of runtime changes to software that would break assumptions that were expressed in the static types. This is not just a matter of throwing some runtime support at it to be able to deal with this.

The ability to ignore types is considered essential by some, and just because this is not the case for you personally doesn't make that fact go away.

You seem to confuse facts with opinions. Just because people think something, does not make it true. But we probably won't agree on this, so I'll leave it be.

There are cases of runtime changes to software that would break assumptions that were expressed in the static types.

Do you have an example we can review?

The ability to ignore types is considered essential by some, and just because this is not the case for you personally doesn't make that fact go away.

You seem to confuse facts with opinions.

No, I don't. Read again what I wrote.

There are cases of runtime changes to software that would break assumptions that were expressed in the static types.

Do you have an example we can review?

Here is a Common Lisp program:

(defclass c () ())

(defun test ()
  (let ((o (make-instance 'c)))
    (print (p o))))

(p o) is presumably a property of an instance of class c, yet the program does not specify anywhere what that property would be. I don't think any static type system will ever be devised that accepts this code.

Here is a transcript of an interaction with a Lisp system that loaded this program:

> (test)

Error: Undefined function P called with arguments (#[C 200D97CF]).
  1 (continue) Try invoking P again.
  2 Return some values from the call to P.
  3 Try invoking SYSTEM::P with the same arguments.
  4 Set the symbol-function of P to the symbol-function of SYSTEM::P.
  5 Try invoking something other than P with the same arguments.
  6 Set the symbol-function of P to another function.
  7 (abort) Return to level 0.
  8 Return to top loop level 0.

Type :b for backtrace, :c [option number] to proceed,  or :? for other options

: 1 > (defclass c () ((p :reader p)))
#[STANDARD-CLASS C 2158A2C7]

: 1 > :c

Error: The slot P is unbound in the object #[C 200D97CF] (an instance of class #[STANDARD-CLASS C 2158A2C7]).
  1 (continue) Try reading slot P again.
  2 Specify a value to use this time for slot P.
  3 Specify a value to set slot P to.
  4 (abort) Return to level 0.
  5 Return to top loop level 0.

Type :b for backtrace, :c [option number] to proceed,  or :? for other options

: 1 > :c 3

Enter a form to be evaluated: 42

42 

This transcript shows a well-specified interaction with the system, based on the original program given above. It is, of course, a silly example, but it illustrates an important concept. (More examples are possible, including cases where properties are removed instead of added.)

Being able to modify a running program on the fly is considered essential by some at least for exploratory programming. It is also considered essential in some circumstances where programs need to be adapted to unexpected requirement changes, where the ability to do this without shutting down and restarting the systems is an advantage.

There is no such thing as 'fully' unanticipated software evolution at runtime, but in some cases, the more flexibility you can have, the better.

Only if you can show me a static type system that allows me to express such kinds of interactions will I believe that it gives me the same power as a dynamic language.

Modifying a running programming is a good example of something that's currently difficult or impossible in most statically typed programming languages. It's also an example of something that (IMO) will eventually be more powerful in statically typed languages, because such languages have a better handle on the organization of the running computation and data. Dynamic languages complect (!) things that are logically phase separated. That makes it easier to slap out simple run-time modification features, but harder to do some of the run-time modification that we'd actually like.

Only if you can show me a static type system that allows me to express such kinds of interactions will I believe that it gives me the same power as a dynamic language.

Quite a Pharisaical demand, Doubting Thomas!

Someone correct me if I am wrong, but I think IRC #haskell's Lambdabot is supposed to be the real world example you are looking for.

It's worth thinking about what kind of guarantees we want an exploratory programming system to provide. In your transcript, you do not have any concurrently executing actors sending each other messages. There are no autonomous interactions, and no open-ended feedback loops increasing the entropy of your system. It's pretty trivial for the sequential case to enforce hot code swapping, but what if tons of stuff is flying around sending messages places?

So if you notice what I am doing here, is I am trying to extend your semantic requirements for exploratory programming and generalize them to concurrent settings. And then I am asking questions that might have no absolute answer, only optimal solutions and margins of error. For the latter requirement extension, neither dynamic type systems nor static type systems handle that stuff today (what Matt M said). But they could. Why wouldn't you want to prove that a server always does its best to serve its clients, even under harsh conditions like automated distributed code upgrades, and why wouldn't you want a detailed prediction of what would happen? The closest thing computer science has today to these sorts of systems are called "automated truth maintenance systems" (a very cool concept, pioneered by McCarthy and others).

Speaking as somebody who loves the White Mountains and once got lost late at night, part of exploring well is having a Life+Gear Wings Of Life backpack, for safety. Same concept applies here. Type systems are in general orthogonal to exploration. Just as a backpack is orthogonal to your feet climbing up and down a mountain path.

Here's a neat quote I saved a long time ago:

Like any new and powerful language feature, Mesa's signal mechanism, especially the Unwind option, should be approached with caution. Because it is in the language, one cannot always be certain that a procedure call returns, even if he is not using signals himself. Every call on an external procedure must be regarded as an exit from your module, and you must clean things up before calling the procedure, or include a catch phrase to clean things up in the event that a signal occurs. It is hard to take this stricture seriously because it is really a hassle, especially considering the fact that the use of signals is fairly rare, and their actual exercise even rarer. Because signals are rare there is hardly any reinforcement for following the strict signal policy: i.e., you will hardly ever hear anyone say 'I'm really glad I put that catch phrase in there; otherwise my program would never work.' The point is that the program will work quite well for a long time without these precautions. The bug will not be found until long after the system is running in Peoria. ... It should be noted that Mesa is far superior to most languages in this area. In principle, by using enough catch phrases, one can keep control from getting away. The non-local transfers allowed by most Algol-like languages preclude such control. It has been suggested that systems programming is like mountaineering: One should not always react to surprises by jumping: it could make things worse. -- Jim Morris, 1976 private communication with Jim Horning, in Computing systems reliability, eds. Anderson, T. and Randell, B., pg 127

The ability to ignore types is considered essential by some, and just because this is not the case for you personally doesn't make that fact go away.

A consideration is an opinion, that you have claimed is a fact. How is this not confusing facts with opinions? Just because they consider it essential, doesn't mean they are right. Your are claiming here that there is no scenario where these people are wrong about types.

Only if you can show me a static type system that allows me to express such kinds of interactions will I believe that it gives me the same power as a dynamic language.

From my local collection of papers on live upgrade:

1. Dynamic Software Updating (2001) -- type-safe live upgrade for C
2. Type-Based Hot Swapping of Running Modules (2001) -- language agnostic
3. Mutatis Mutandis: Safe and predictable dynamic software updating (2007) -- a more rigourous follow-up to the first paper
4. UpgradeJ: Incremental Typechecking for Class Upgrades (2008) -- live upgrade for Java-like languages based on a minimal runtime architecture
5. Abstract Machines for Dynamic Computation (2001) -- live upgrade for SML (and Java)
6. Dynamic applications from the ground up (2005) -- Haskell solution using explicit upgrade IIRC, which John (Z-Bo) mentioned below (Lambdabot, Yi)
7. Mike Hicks provides a list of other work here on LtU -- Hicks is the author of some of the above papers

All of the above papers providing implicit upgrade require only runtime support, and many of them have been applied to real production systems. Hicks' work has been used with OpenSSH and FTP daemons, for instance.

Providing live upgrade via explicit means has been straightforward since the invention of continuations. Every safe upgrade point is simply a continuation where the program specifies the persistent state together with state serializers which are invoked in case of upgrade.

Many of the above papers make this explicit solution implicit by disbursing these upgrade points throughout a program automatically, like GC safe points.

The reason these solutions aren't widely used is simple: there hasn't been a compelling need. Most production services are stateless and use external persistence mechanisms, like databases, which have their own schema upgrade process, and so service and schema can evolve somewhat independently (only sometimes requiring coordination).

Service upgrade is handled at a more coarse grained level, ie. spin up a new instance, redirect traffic to it, take down the old one for upgrade. This separates the administrative concerns from the software development concerns. I'm not convinced these concerns will ever converge fully, and so I'm not convinced live upgrade is needed as much as is sometimes claimed.

As I read that sentence, fact refers to the consideration that the ability to ignore types is essential. Then again, English is not my first language.

OCaml's structural objects throws type information away behind an existential. Extensible records do not, so they are strictly more general.

That is not true. OCaml's objects are polymorphic records -- row variables will be universally quantified, unless you use an explicit upcast.

However, OCaml doesn't have all the record operations that are described in the paper, nor the dual case operations.

Been awhile since I looked into this, but I was certain that OCaml objects didn't natively support binary methods. This seems to support that view, since binary methods must be encoded via a public type parameter. This says to me that the record type is hidden, so what am I missing?

I think you are misreading the code. The page shows how you can express them. There is no public type parameter, just an (internal) self type.

In any case, that is a somewhat different problem than just having record polymorphism. Here is a simple example of universal quantification:

# let f x = x#a; x;;
val f : (< a : 'b; .. > as 'a) -> 'a = <fun>
# let o = f (object method a = (); method b = 4 end);;
val o : < a : unit; b : int > = <obj>

Note how the dots represent a (universal) row variable. Unfolded and made explicit, the type of f actually is ∀ 'b 'r. < a : 'b; 'r > -> < a : 'b; 'r >. Now, if only the syntax for object literals was less verbose...