Lambda the Ultimate

That seems odd considering making undesirable outcomes inexpressible is a primary motivation for types.

It's the old meta- and object-logic debate we also had with Hewitt. The fact that you blocked an argument doesn't imply you blocked all arguments, and even the fact that something cannot be proven anymore in an object logic is problematic when you consider it can still be proven in a more expressive meta-logic. Even if you consider that object-logic should conflate with meta-logic.

I don't know exactly what they did. I don't feel like reading the argument that close, that would take months for me, but I can't say I trust this result that much. More, since it seems to 'disprove' something which is generally accepted; where disprove is between quotes since I don't know what they did exactly.

Classic "theorems" like Gödel's often aren't really theorems in the limited prosaic sense of something you could run through, say, Coq; they're deep insights. In Gödel's case, the really deep insight was that types can't protect a formal system against the incompleteness/inconsistency problem because types, unless they actually cripple the power of the system, can only prevent the system from acknowledging that it has a problem, they don't prevent the problem from being there. This paper might be getting around its problem by a legitimately clever technique, but the abstract fails to get that accross — it makes it sound as if they're claiming to block a proof with a gag order, which is in essence what Gödel realized doesn't work.

Gödel proved that a logic can't prove its own consistency, so you just need a self-interpreter that doesn't prove consistency. As shown in other work (and not discussed here), usually an interpreter lets you prove consistency — that is, it lets you prove that the object language cannot express object-level proofs of absurdity. If you have a term `e : Expr EmptyType` (an object-level proof of absurdity), with a typed interpreter you can produce a term `interp e : EmptyType`, which is absurd.

However, the correctness theorem of their interpreter is more restricted — it guarantees that `interp (quote e)` reduces to `e`. So the above proof needs the extra hypothesis `e: EmptyType` to produce a proof of `EmptyType` — so we end up proving `EmptyType -> EmptyType`, which is quite true.

They don't claim to disprove Gödel (and barely mention it) — in fact, the "normalization barrier" has never been stated formally anywhere to my knowledge. (I've tried formalizing it with my colleagues for some time, and had run into some of the loopholes they're using).

Also, there's a huge difference with Hewitt: not only this was accepted by peer review at a reputable venue, but their code and proofs can be downloaded.

(At best, there's the remote possibility of a bug in their FOmega typechecker that their code happens to exploit and that nobody who understood the paper caught, but that seems very unlikely, also because it is well understood how to implement one).

If you block an argument that doesn't imply you blocked all arguments.

I simply don't like that part of their argument as it was stated in the article. Possibly, it is phrased in a manner which doesn't do justice to their technical argument. I wouldn't know, I am not going to read this paper.

(Let's not discuss Hewitt.)

You might have a point on the phrasing, or not. But it's not so productive to get to the bottom of that hole, so let's set that aside and get on the content.

In this case, arguably, there's only one actual argument suggesting what they did is impossible: a total self-interpreter for a total language is impossible. But if one looks at the actual statement, it doesn't actually forbid their scenario. And if you try to apply *the* known proof, it fails for typing reasons: the proof depends crucially on creating some specific term in the object language, and that term is ill-typed. Gödel didn't prove that you can circumvent all typing restrictions.

You can imagine other attempts to prove the same theorem, but they exhibit their self-interpreter I. So assuming mathematics is consistent, attempts to prove that I doesn't exist will fail. To be sure that I exists, you can just look at I, you don't need to look at each proof in detail; you can still do it, but for other reasons (like I do in another comment).

Also, there's a huge difference with Hewitt: not only this was accepted by peer review at a reputable venue, but their code and proofs can be downloaded.

Hewitt is making a pretty simple claim that shouldn't be all that controversial but this forum reacted very disappointingly.

I just skimmed the introduction and conclusion, but I think they do claim to implement beta-reduction. Section 9-Terminology distinguishes between two types of self-interpreters. An "unquoter" takes an AST and returns the value it represents (unquote "2+2" --> 4), while a "self-reducer" takes and AST and returns an AST of the value it represents (self-reduce "2+2" --> "4"). They claim to implement the former.

I thought they realized an unquoter, so in the strict sense, unquote "2+2" -> 2+2, which finally reduces to 4 within the system.

I guess an unquoter is more than sufficient, even more ideal, than an interpreter.

Still not sure what they aim to do. At worst, if they can prove to do something which should really be forbidden, they broke some important logics, chaos reigns, and people are back to sticks and stones; i.e., you can only prove what you can calculate.

Eh, I don't think it's that bad. :) They work in the standard System Fω, which is a very well understood language, and definitely sound. So I don't think this "loophole" will lead to any logical inconsistency. I think the main conclusion is that the definition of "self interpreter" gives a little more wiggle room than you would think.

I think the main limitation is that, as they write, their quotation function can not be written in System Fω. That is, you can't write an interpreter that takes an Fω program written as a string and evaluates it to a value. Instead, first you have to take the string and "quote" it as a value in their clever representation, and then you can evaluate that value, but the quotation step happens outside the system.

This is particularly clear if you think about their "cheating" encoding in Section 3.3, where a program is encoded as just that program itself with a few extra identity functions scattered through it. If you tried to to write a program which converted from strings into that representation, basically you would have to take strings like "(λn. n+2)" and convert them to functions like (λn. n+2). That is, you would have to write an "ordinary" self-interpreter, which we know is impossible! :)

Does this mean the have banned reflection, as you can't turn code into an interpretable string?

Edit: That doesn't seem right now, its more like you cannot interpret flat strings, but you can interpret some other structured syntax. Could you write something that converted from the language AST to the quoted format? Then reflection would still be possible. In that case you could introduce a display transformation that inserts the quoting, and then the code the user inputs would look the same as when it is displayed. Does it really matter that the code is not representable as a flat string within the language itself?

I'm not sure how you define reflection; the goal here is to support reflection on typed code (at least, that was the goal when my colleague Tillmann introduced typed self representation with my boss).

I think you can do reflection as long as you start from "typed" syntax, but (I believe) you can't go from untyped syntax to typed syntax (the "quoted" format) *in general*.

There shouldn't be any interesting difference between different untyped syntaxes, ranging from Gödel codes to strings to ASTs, so let's pick Gödel codes.

A typed interpreter takes Expr t to t (or, technically Expr (\overline{t}) to t); Expr t is the typed syntax, and t is a type variable. If you could go from a Gödel code to Expr t (for the right t), then you could evaluate the result with the typed interpreter, and you'd have a total language with an untyped self-interpreter — which we know from computability is impossible (as they describe in Sec. 3.1). So you can't get from Gödel codes to typed syntax in general — I like to say, you can't write a self-typechecker.

While (IIRC) the paper doesn't show how to combine typed syntax together, you can write some combinators, and use them if you have enough input. For instance, if `a` is an `Expr (T1 -> T2)`, and `b` is an `Expr T1`, you should be able to apply `a` to `b`.

On the other hand, if you don't know well the types of `a` and `b`, you can't match on the types (as far as I can tell) and check if they're compatible. That's I think a likely problem in practice if you try writing a self-typechecker. If you add a value-level representation of types, you get different problems.

I think the operations you want are easy to implement if the representation of lambda term X is a pair (Godel number of X, normal form of X). To compose two of those, just compose the normal forms and concatenate the Godel numbers. Other operations like eval or pretty printing are also trivial. Or am I missing something and their "typed syntax" has more interesting desiderata?

The typing is really really hard. A typed interpreter for a language with addition, say, and pairs (and nothing else) usually requires GADTs or Church-encoding. I recommend you try or look up answers.
Now you want to represent polymorphic functions in this typed syntax, in such a way that you can apply them and get the right type.

And once you have the self-interpreter, you need to make sure that you can also write and type other operations — and in many attempts, that's often only possible for some operations but not others. Their set of benchmarks is the most successful ever.

All you have explained is the easy part (and I'm not sure "concatenate Gödel numbers" is quite correct, but some actual operation exists).

Thanks, I think I understand the paper a bit better now. Here's a quick recap, just to make sure I got everything right:

Since we provably can't have an eval function that accepts a program's source code (Godel number), we will instead make it accept a "typed representation" - a value of some type Expr<T> where T is the program's return type. The main requirement is that all constructible values of type Expr<T> must be in one-to-one correspondence with valid programs that return T. (That means you can't just represent a program by its return value, or its return value paired with its source code, etc.)

With such a typed representation, the problem becomes much simpler. The usual counterexample with diagonalization no longer typechecks, and writing a self-interpreter in the most direct and obvious way will just work (section 3.3 of the paper). The main unsolvable problem was actually going from the source code to the typed representation, which is less like source code and more like verified executable code with a bunch of annotations.

From that point, the game is about how many "annotations" you can stick in. I suppose it's pretty exciting but I haven't parsed that part yet. Overall, good paper, though it's way too easy to misunderstand.

What's described in Sec. 3.3 is not what I'd call the most obvious self-interpreter — (though maybe you did understand what happens and just have different expectations). Regardless, I'll give my summary of 3.3: it's a trivial self-interpreter, but it gives a counterexample to the supposed "normalization barrier" and you can explain it quickly to anybody understanding System F (at least on a whiteboard, I'll try here).

As they say there,

The quoter [described in this Section] will support only the self-interpreter and nothing else.

In particular, on that representation you can't do anything else you'd expect to do on an AST — say, pattern matching or transformations. The representation is a function `\id -> body`, and as they say, you can prove that the `id` argument must be the polymorphic identity function (Haskell's id) by parametricity.

In very imprecise terms, the quoted program uses id as a strange sort of callback.
The goal is that quoting always produces a normal form.
For instance, take program `(\x -> (+) x 1) 41`. Evaluating it would reduce to 42, but if you quote it you get `\id : ... . (id (\x -> (id ((id (+)) x) 1))) 41`, where each application is stuck until you get the `id` argument. The self-interpreter simply provides that argument.

I find it hard to call this "obvious way" — if you want, it's the most extreme form of metacircular interpretation, but somehow people seldom discuss this.
As they say, this result (unlike the other ones) holds also for System F and for bigger systems, while the main self-interpreter they provide is just for Fomega, not for smaller or bigger systems.

For a preview of the rest, I suggest you to skip a bit to Sec. 7 and see which operations they implement. They'll probably look somewhat obvious (except maybe the CPS transformation); yet, they're the first to support all of them at the same time.

Also, people have used a typed representation for much longer, so that's not enough to solve all problems. The other big problem is described in Sec. 4 (though I already forgot Sec. 4.2 again).

Yeah, I understood the interpreter from section 3.3 in the same way as you describe. It comes together easily once you see that it should only support eval, and it's very natural that it would work in many different systems. Actually it seemed more fundamental to me than the main result, because the problem solved by the main result is not as concisely specified, unless I'm missing something.

Just something which I wondered about.

Thanks for the summary. I want to read the details sometime to see how it relates to what I've written about. Sounds like this moves 'encode' out of the language, whereas I move a tiny part of eval out of the language.