Lambda the Ultimate

I like the look of this, it avoids the redundancy, but it takes a lot of space and I am not sure how easy it is to read with a 1000 line program. Generally I have a preference for large files/programs to use a format that is not spatial, and does not require layout. However it would be nice if the format were regular enough that an external tool could parse it and render a pretty graphical derivation, or convert to MathML.

Reading the type derivation as a proof of type, it seems fairly standard to replace the "-----" horizontal line with a turnstile "|-" (see the proofs any type-theory section of the wikipedia page on natural-deduction http://en.wikipedia.org/wiki/Natural_deduction

That would suggest a notation like:

var: x:{x:a}|-a, var: y:{y:a}|-a, app: x y:{x:(a->b),y:a}|-b |- b

The HM example from Wikipedia is kind of what I was thinking of, but I don't like the table formatting - it will cause problems with large programs that have long types.

So I guess a requirement is that it is not 'table' or 'tree' formatted, but a series of statements on multiple lines.

So substituting "------" for "|-" seems reasonable, or is there a better character for this? Numbering the statements seems common, and avoids repeating the typings, so I ended up with:

1) var |- x : {x : a} |- a
2) var |- y : {y : a} |- a
3) app (1) (2) |- (x y) : {x : (a -> b), y : a} |- b
4) var |- z : {z : a} |- a
5) app (3) (4) |- ((x y) z) : {x : (a -> (b -> c)), y : a, z : b} |- c

I then thought having the two judgement symbols was confusing...

And I guess you're right that there is a good argument to expose the reasoning first and then show the derived fact. In math that would make the derivation harder to check, but anyway, in this case, the derivation is mechanic.

You'll get academic flak for the double turnstile. I would suggest to just use something which separates but has no conventional meaning.

Twelf would write this something like this:

(app (((x y) z) : {x : (a -> (b -> c)), y : a, z : b} |- c)
   (var (z : {z : a} |- a)
   (app ((x y) : {x : (a -> b), y : a} |- b)
      (var (y : {y : a} |- a))
      (var (x : {x : a} |- a))))

Which again looks nice, but all those nested brackets are going to get painful in long proofs, but it is nice if you want to express proofs in machine readable syntax, or include them in programs, and having a single uniform syntax for it would make sense. I guess a compromise might be to allow meta-variables like this (and changing the argument order):

X = var (x : {x : a} |- a)
Y = var (y : {y : a} |- a)
A = app X Y ((x y) : {x : (a -> b), y : a} |- b)
Z = var (z : {z : a} |- a)
app A Z (((x y) z) : {x : (a -> (b -> c)), y : a, z : b} |- c)

But as I am getting older adapting to new notations makes me grumpy like anyone else.

I would do it like this.

1. [var]          x : {x : a} |- a
2. [var]          y : {y : a} |- a
3. [app (1) (2)]  (x y) : {x : (a -> b), y : a} |- b
4. [var]          z : {z : a} |- a
5. [app (3) (4)]  ((x y) z) : {x : (a -> (b -> c)), y : a, z : b} |- c

A dot is easier on the eyes and I find square brackets usually more readable than curly braces.

I like this, and am going to use for now. I have a feeling I might want a unified proof notation later (as the type derivation is just a proof trail of the logic program with clauses var/app/abs etc) so I might move to something like the Twelf notation later (in which case the version with meta-variables seems nicer as it avoids all those nested brackets)

I think the above is the right title which shows a manner of giving forward nested proofs. The problem with the Twelf representation being that you probably can't keep track of the indentation whereas Lamport's solution gives you nested series of numbers to keep track of. I'll see if I can find the paper somewhere.

The original: http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-how-to-write.pdf

An updated version from 2011: http://research.microsoft.com/en-us/um/people/lamport/pubs/proof.pdf

You can't do the alignment without a complete pass through the results to find the longest variable name (because of let and abs), which puts me off doing that, so I have done it without alignment for now. Mainly because the parser builds the terms in the same order that we compositionally do type inference:

parsing:
var: succ(x : |- ) @1(0)
var: succ(y : |- ) @3(0)
app: succ((x y) : |- ) @3(0)
var: succ(z : |- ) @5(0)
app: succ(((x y) z) : |- ) @5(0)

inference:
1. [var] x : {x : a} |- a
2. [var] y : {y : a} |- a
3. [app (1) (2)] (x y) : {x : (a -> b), y : a} |- b
4. [var] z : {z : a} |- a
5. [app (3) (4)] ((x y) z) : {x : (a -> (b -> c)), y : a, z : b} |- c

So I want to do the type inference as the tree is constructed, so after parsing we have the typed tree, and have the types available to help debug errors from parsing.

Is the purpose of this debugging your code or producing actual error messages for end users? I don't think I'd ever want to see such verbose reports. If the AST isn't well balanced, you end up with quadratic repetition of assumptions. I'd rather see a presentation that just tells me what was unified between sub-terms.

Its primarily for debugging at this stage, but as the derivation is attached to the AST nodes, fragments of it may be helpful.

I agree about the unifications. At the moment the unification code I am using doesn't produce the unifications as output, it directly updates the union-find graph. I have some unification code that does as part of the logic meta-language, and longer term this is the way forward, but I need to understand the naming issue first (that is why higher order logic, or nominal unification are required to express type inference in a logic language).