Lambda the Ultimate

It's well understood in the community that discusses the "expression problem" that this is essentially an interesting issue in type theory. The more-or-less standard solution is often referred to as "virtual types." One of the earliest approaches to virtual types was Beta's virtual classes, but these weren't type-safe. Relatively recently (2000), Didier Rémy and Jérôme Vouillon published On the (un)reality of virtual types, in which they observe that the combination of parametric polymorphism, correct typing of binary methods, and structural typing are sufficient to allow for the construction of type-safe virtual types. Their extensive examples are in O'Caml. I found the following comment in the introduction humorous:

In fact, using Ocaml as the implementation language, all examples that we know as involving virtual types can actually be typed in with no effort at all. Actually, the untyped code that one naturally writes needs only to be documented with class type parameters and, sometimes, with type constraints. No other change in the code is necessary. Had we not known about this challenge, we would not have noticed any particular difficulty.

Still, as you rightly point out, it's good to see this being tackled by the Haskell community.

Update: I also recommend Independently Extensible Solutions to the Expression Problem, which wonderfully summarizes the issues and addresses them using Scala as its vehicle. I continue to believe that O'Caml and Scala are the two best languages to become familiar with today—I find them considerably more approachable than Haskell, for a variety of reasons.

Qrczak: Actual dictionaries are usually polymorphic to various degrees.

Right again. Here's a Polymorphic Map for O'Caml.

The paper you mention (Independently Extensible Solutions...) was a little strange to me in that they cast everything in terms of the "Interpreter" and "Visitor" design patterns.

Is this normal practice? It seems like this expression "problem" has nothing inherently tied to design patterns.

dbfaken: The paper you mention (Independently Extensible Solutions...) was a little strange to me in that they cast everything in terms of the "Interpreter" and "Visitor" design patterns.

Is this normal practice? It seems like this expression "problem" has nothing inherently tied to design patterns.

Upon re-reading the paper, my sense is that they're just attempting to articulate how the expression problem has actually been tackled in languages that don't lend themselves to implementing virtual types. They're not trying to be doctrinaire; they're saying "Solutions with an OO flavor tend to rely on the interpreter pattern and solutions with a functional flavor tend to rely on the visitor pattern," and describing the limitations that arise from both approaches. This certainly reflects my own experience with attempting to address the expression problem in popular programming languages. But the sheer amount of material they were able to write on the suboptimal solution space reinforced the humor that I found in the comment that I quoted from "On the (un)reality of virtual types," in which the authors, using O'Caml, noted that they wouldn't have known there was a "problem" if they hadn't been told about it.

OK, thanks. That makes more sense.

sjoerd_visscher: To me it's so obvious that you want this, that I'd say: drop the open syntax, and just make all types and functions open.

I immediately have two objections:

1. Saying "As an OO type of person" ignores the paper's observation that a straight OO approach makes it difficult to add new functions to the system without modifying base classes.
2. I want the ability to say "this isn't extensible." In the real world, not everything is. In particular, it isn't always practical to design for unanticipated extension. Not every member function in C++ should be "virtual;" many classes and methods in Java should be "final."

Re 1: Right, maybe I simply should have said: "As a Javascript programmer"

Re 2: In the case of stateful code I agree. But in this case I think you don't even have to design for extension. It is the responsibility of the extender of the data type to implement all the functions that have the data type as input.

That fundamentally messes up some existing properties of the relevant type systems, you'd never be able to tell a function was total again.

How is making everything open different for type systems from just adding the open feature?

Being able to selectively say "this function is open," i.e. may not terminate, is one thing. Saying "all functions are open," i.e. may not terminate, is another thing entirely. One thing that type systems do is constrain terms such that progress in their evaluation can be guaranteed. This naturally means that type systems have to be careful in the presence of general recursion, i.e. of "openness." If you make everything open, it quite literally means that you don't care about guaranteeing progress before delivering your software. That's not an indefensible position, but neither is it one that many of us are willing to adopt.

The paper does not even mention termination.

sjoerd_visscher: Are we talking about the same openness?

Not directly, and I have to apologize for the confusion. They use "open" to mean "extensible," and that's it, as far as what's explicitly said in the paper is concerned. However, the moment you have an "extensible function" in a language with general recursion, you open (sorry) yourself up to what in some texts is called "divergence" and more often is called "non-termination." It's exactly what Philippa meant when she said "you could no longer prove that any function was total," because total functions don't diverge, i.e. they're guaranteed to terminate.

sjoerd_visscher: The paper does not even mention termination.

No, it's implicit, as described above. You should go through life with the implicit understanding that general recursion gives type theorists the vapors because of the risk of non-termination; that allowing arbitrary overloading of functions in languages with general recursion means that you run the risk of introducing general recursion, and hence non-termination, where it isn't wanted; and that having "open functions" implies arbitrary overloading of functions. :-)

The papers says the idea can be implemented with a source-to-source transformation, the result being regular Haskell code. So if the target of the transformation is guaranteed to terminate, so is the input of the transformation, unless the transformation itself would not terminate. But that clearly isn't the case (it's a very simple transformation).

Termination isn't guaranteed by the type system alone. But the type system does currently guarantee that you don't get passed a constructor you weren't expecting and fail a pattern-match. If everything's open, it can't make that guarantee, and (to give an example) you could add a new constructor to the standard list type and watch a pile of previously-total functions with no clue said constructor exists fall over. Adding a new case to every function on lists isn't practical either, if nothing else some of them will be unexported functions inside other modules.

Every type includes ⊥. There is little difference between encountering an unknown constructor and encountering ⊥; you can pass it around, but you can't look inside. Open types don't change anyting wrt. safety in Haskell.

The only difference is that with closed functions you know that e.g. length either returns a non-negative integer or ⊥, and thus various equivalences in code using length hold (e.g. that comparing the result for being non-zero is the same as comparing it for being greater than zero) which would no longer hold with open functions, so some implementation details would become visible.

There's one significant difference: one can knowingly avoid passing ⊥ to a strict function. Sure, functions can attempt to default on constructors they don't know about, but that doesn't always make sense.

There are rules certain functions have to follow. length will always have to return a non-negative integer or ⊥, open or not, that's what the semantics of the function requires. Unit testing can be used to ensure that is the case.

I don't see the problem. In the OO world it is not unusual to implement the Collection interface, which I think is the equivalent of adding a new constructor to the standard list type.

If there are unexported functions inside other modules, I'm sure the type system would complain. Which would make certain modules unusable with certain extensions, but that's better than no extension at all.

Btw, I'm sure there are methods in the standard Java library that won't terminate when passed the wrong implementation. I've never heared anybody complain about that.

No, implementing Collection isn't equivalent to adding a new constructor to [] - pattern-matching on algebraic datatypes comes about because more of their concrete structure is exposed. The equivalent of implementing Collection in Haskell'd be providing an instance of a Collection type class - something which can already be done.

If I ever found one, I'd complain about it!

But what if you implement a Collection by inheriting from AbstractCollection, that generates the fibonacci series as an Iterator. Then do a .contains(-1) on an instance.

This suggests to me the need for an AbstractFiniteCollection which adds termination guarantees for operations like contains. That's exactly the kind of property that still can't be maintained for what're essentially open discriminated unions when structures're defined not just by individual constructors but by the interactions between them (consider what happens to the standard list type if you take out the nil constructor, or correspondingly to a stream when you add it!).

http://haskell.org/haskellwiki/Extensible_datatypes

Maude and the OBJ family all fall loosely into the category of theorem provers, and have unusually rich type systems featuring dependent types. They have strictly more expressive power even than Epigram, let alone Haskell or O'Caml or Scala, nevermind Java, C++, Python... they definitely also make different choices about starting from an open or closed perspective, since they want to be able to support whatever can be proved in either context. e.g., if you want to prove that a function is total, you can. They're rich metalanguages implementing, thanks to the Curry-Howard Isomorphism, rich logics.

The OBJ stuff sounds neat to me, but I'm pretty un-smart when it comes to PLT, and so I'm unsure what they would/not be used for: the apps I've seen mentioned are all proof-esque things, rather than 'down to earth' applications. Would e.g. Maude be something one would ever want to use to write their next video game server or whatever? I'm just trying to get a feel for it all since I'm unlikely to actually understand the details.

You probably wouldn't use Maude or Obj or Coq or Isabelle or MetaPRL to develop the Unreal 4 technology. What you might do, however, is use one of them to prove that certain properties of UnrealScript 4 or the new anti-cheating architecture hold. One of the things that I've mentioned to Tim Sweeney is a desire to do just that: to use, e.g. MetaPRL to formalize the design of his new language, perhaps even going so far as to develop a certified compiler for it, since the ability to do so is an explicit design goal for MetaPRL, and because the MetaPRL team is relatively local to me.

OK, thanks for the clarification! It is what I suspected from the docs I'd read about Maude and things written with it. There's an interesting division between having annotations (e.g. JML) in your code, and having very separate languages & systems. I don't have deep experience with either I did do some 'zed' back in my abortive grad school years), so I can't say if they are light-years apart. Certainly with JML you are restricted to what it supports, so you can't use 1.5 or Scala with it. External systems might provide one with a way to be more flexible. It sounds like one would design a system in the modeling / proof language, and then once that it all worked out make an implementation in Java/C++/whatever. The thing is, you immediately get into the problem of drift between your logical and proven spec, and the 'real' implementation?

Even though I profess to know nothing, if you convince Mr. Sweeney, please hire me as your lackey. ;-) It would be amazing to learn this stuff via the (possibly) fun path of games.

raould: External systems might provide one with a way to be more flexible. It sounds like one would design a system in the modeling / proof language, and then once that it all worked out make an implementation in Java/C++/whatever. The thing is, you immediately get into the problem of drift between your logical and proven spec, and the 'real' implementation?

That's exactly right, which is a major reason why environments like MetaPRL are attempting to be not only theorem provers, but more extensive logical programming environments such that you can actually write a compiler for your language in them. Of course, this still begs the question as to why you should trust the portions of the proof engine that are written in the language that the proof engine is written in, so MetaPRL, and presumably other tools like it, include a formalization of (a subset of) O'Caml so that you can actually prove things about code written in that subset.

In practice, though, most people just don't care that much, so you're right: most people who even care enough to prove properties of algorithms and data structures with a theorem prover go ahead and do the actual implementation in Java/C++/whatever—languages for which a formal semantics doesn't even exist—and we simply hope that they know what they're doing.

The thing is, you immediately get into the problem of drift between your logical and proven spec, and the 'real' implementation?

right, so the other tactic is to try extend a "real" language using ideas from a theorem prover, trying to find the right balance between expressive power and complexitiy. that's what is discussed in this thesis (a more coherent view of the final result, omega, is in this amazing paper (discussed several times here))

(and the thesis includes some "down to earth" discussion, imho).

Does anyone have advice for where a person should begin to learn about things like Maude/OBJ/MetaPRL? Something like a tutorial level text, which covers the basic theory, but which also uses a particular concrete implementation to teach the syntax/system/idioms, and to help keep things grounded for a beginner. For example, if a person wanted to learn about functional programming in general, I might recommend Haskell and The Haskell School of Expression.

Or is this an area of study that isn't really (yet?) accessible to someone without an advanced degree in mathematics/compsci?

Maude has a very nice-looking (I haven't worked through it) Primer available. In fact, as a non-user, the most impressive-looking thing about Maude is its documentation, although CINNI and the Open Calculus of Constructions sound awfully interesting, too.

OBJ3 has Introducing Obj. Once again, I haven't actually worked through this. If you do happen to use OBJ3, please tell Joe Kiniry I said howdy. :-)

MetaPRL has a tutorial that's a work in progress, but I've found pretty easy going. Of course, I'm already an O'Camler, and if I really get stuck, I'm an hour's drive away from the team at CalTech. MetaPRL also benefits from having actually been used to develop a compiler or two, so if your interest is in programming language semantics, MetaPRL is highly recommended.

Coq is another prover written in O'Caml. It has an extensive set of libraries, a book "Coq'Art," and has been used to prove security properties of a methodology in conjunction with Java Card technology.

Twelf is another prover with a particular focus on programming language semantics. This one's in Standard ML rather than O'Caml. In some sense the "granddaddy" of the programming language theorem provers, with its connections to LF and Elf, which are venerable names in this space. There's a correspondingly rich literature on LF/Elf/Twelf, but it's unfortunately also correspondingly less accessible than the alternatives—some of the newer systems seem to have been more influenced by Tom Melham's observation that "Formal methods will only succeed when they can be used by people who don't understand them," and attempt to close that gap with tutorials and generally better documentation.

All of this is, of course, IMHO, YMMV, IANAL, etc. etc. etc.

I'm getting a lot of mileage out of A Maude Tutorial - M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-Oliet, J. Meseguer, and J. Quesada found via Papers on Maude and Rewriting Logic.