Lambda the Ultimate

(This will be the third thread in the last few weeks where I've chimed in with "hey, this sounds like something I'm working on", but here I go again, with apologies...)

In my logic / language core there is also a single Term that encompasses both types and values. I want to be sure it's consistent (I think I can prove the predicative fragment consistent and I have a plan for proving the impredicative fragment consistent) and then I'll release a description of the system, but it's very simple and elegant and feels discovered rather than engineered.

Looking through the paper here, though, gives rather the opposite impression. This paper apparently only describes the run-time semantics of the computational fragment of the language, but it's hard to imagine an elegant logic on top of this for proving program properties. I suspect that this complexity will lead to corner cases in the logic / type system, but we'll see.

The combination of low level operations (pointers & heaps) with infinite sets is interesting. And Tim has partnered with a couple of guys from Intel, so maybe we'll be seeing some transfinite processors in the not-to-distant future!

And I wonder if this language carries out the program of a flexible type system that is assigned semantics in this universe of denotations and can thus be verified type safe. I think that's going to turn out to be a good idea. Tim, et al. may be thinking that an elegant system can be built atop this foundation, even if it's not the most elegant piece of mathematics itself.

Finally, I also started with the idea of using sets of terms for types. I recall even arguing with Andreas about it. This seems to be a very old idea that was how most people originally approached types. Then, with advances in type theory and papers like Reynolds' "Polymoprhism is not set theoretic", programming language theorists moved towards type theory and away from set theory. I also decided that the math was telling me the same thing and by switching away from sets of terms to something closer to type theoretic semantics, I ended up with something that had the properties I wanted without the annoying warts. But some of those properties are the ability to reason about things in a way that's much closer to way you'd reason in a naïve set theoretic approach. I definitely understand the appeal of sets.

That idea seems to be combined here with the idea of using singleton types instead of values and thus making everything a set. That's not a road I've been very far down.

I would like to see some documentation for your work at some point. Teasing me with it for almost three years now is unforgivable. :)

The intention with lambda-mu is to layer on a direct effects-typing system which treats general recursion and type:type usage as effects, distinguishing potentially non-terminating constructs from effects-free total constructs.

Thus, there would be a "foundational" subset of the language suitable for proofs-as-programs work. And the potentially non-terminating (but otherwise effects-free) subset would be as suitable as Haskell for weak proofs-as-programs work.

It's easy to get a sound start in this direction: simply raise the non-total effect whenever a recursor or non-wellfounded type is introduced. It's much harder to analyze terms to detect and allow liberal use of wellfounded recursion and to implement the sort of "level polymorphism" that enables the compiler to recognize benign usage of type:type.

I've looked a bit over the just-linked-here paper some, which is really much better as an introduction than the run-time paper.

I have some questions if you're feeling inclined to answer them:

- What do you see as the biggest advantages of the 'types as multi-values' approach? I can see that having operations naturally lifted to types (e.g. Nat < n) is nice.

- You use factorial as an example of staging to prevent the verifier from diverging. Does the staged version check induction? Would it reject the recursion on fact(n - 1) if you changed it to fact(n + 1)?

- How do you handle type:type in the set-theoretic semantics? It looks like the semantics for 'types' is all types (in Figure 1). But then what of terms that impredicatively use 'types'?

Opinion follows

While "proofs as programs" is a great slogan, I think for truth in advertising it should be "proofs as typed programs". I prefer to separate the computational aspect of programs from the types that prove properties about that computation. It's not just that non-terminating programs aren't proofs, but that terminating programs aren't proofs until they're proven to have the correct type.

The advantage of "types as multiple values" is that we can reuse the full expressiveness of the value language to express types. Most importantly, this includes the ability to give variables names such as n:nat and then refer back to them. This gives you recursive dependent types, "very" dependent function types, existentially quantified types, and universally quantified types.

For example, we can represent type type of pairs of natural numbers where the second is the successor to the first as type {n:nat,n+1}.

I think two issues are entangled here. Imagine a system where you can write:

{(n,n+1)}

This reads "set of values of the form (n, n+1)". I can see why you'd want that. You see that kind of thing all over the place in math.

But you've gone further and have dropped the set-of construction that takes you from value land into type land and instead identify values and singleton types. It's this identification that I'm trying to understand.

Paradoxes result not only from the use of type:type but also from the admission of general recursion into the type-language. For lambda-mu as envisioned, it would be most natural to write a "naive set-theoretic semantics" admitting all of the paradoxes that entails.

A more rigorous approach would be to express the set-theoretic semantics in a three-valued logic {true,false,undecidable} and ensure that you can never derive the implication true->false.

It is up to a lambda-mu verifier to ensure the impossibility of deriving a paradox at any verification step in the language's total subset. In the non-total language, paradoxes are admissible and simply coincide with divergence. Here's one: x:int=x+1.

It is up to a lambda-mu verifier to ensure the impossibility of deriving a paradox at any verification step in the language's total subset. In the non-total language, paradoxes are admissible and simply coincide with divergence. Here's one: x:int=x+1.

So I guess this is the same mechanism that answers my other question. The verifier is responsible for rejecting the following, but only if the function is supposed to be total:

bad_fact(n:int):int=if(n==0) 1 else n*bad_fact(n+1)

Does that mean you don't distinguish between inductive data and potentially infinite constructor trees within the type system, but instead let the verifier detect divergent misuse of infinite data? How do you define Nat to ensure that (succ succ succ ...) isn't one?

Thanks, I looked around but didn't find anything, so I assumed it was under the typical ACM embargo.

Wouldn't that put the logic for whether to expand fact(3) in the wrong place? If you have fact written the first way and need to prove fact 3 = 6 at some use site, do you have to change the definition of fact?

Thanks for the explanations thus far.

Why is divergence of compilation a turn off? There's always a human overseeing the compilation process, so if compilation diverges they can just abort, fix the bug in the type-level program, and recompile, no?

How do you know it's a bug and not just a really long compilation?

Isn't a really long compilation ALWAYS a bug?

Most people don't use compilers as theorem provers. So it's usually easy to get a sense of progress.

If any compile-time computation is taking more than a few seconds and not making visible progress, it's buggy and needs redesign (even if it would terminate given more time). For live programming, that 'few seconds' is reduced to 'few milli-seconds'.

(IMO, dealing with a non-termination error at development-time is much easier than dealing with the same at runtime. Therefore, it is somewhat pointless to target the former unless you've already eliminated the latter.)

Isn't a really long compilation ALWAYS a bug?

Depends how much metaprogramming you're doing, or on the size of your program, or on whether the structure of your program is a pathological case for your type inference (HM is worst-case exponential). How can you possibly quantify how long a particular compile should take?

For instance, you could write a metaprogram to evaluate factorial(1000). This is more difficult to do in C++ with templates, even though they're Turing complete, but we're considering expressive languages that unify types and terms, so shooting yourself in the foot is correspondingly going to become much easier.

If any compile-time computation is taking more than a few seconds and not making visible progress

What constitutes visible progress for compilation?

How can you possibly quantify how long a particular compile should take?

At least two ways.

First, you can study performance the exact same way you quantify and comprehend how long any runtime program would take. It is not uncommon to study performance of algorithms in Turing Complete languages. This is no different.

Second, you can quantify by external requirements. These are especially easy in live coding systems. But even in more 'traditional' environments, one can judge based on software engineering concerns (e.g. $ cost per second of compile time, gains from a more rapid cycle, is it worth the time), human factors (loss of flow, distraction), UI factors, etc..

...

I suppose that, if you use a different paradigm for compile-time that has less predictable performance, you might have problems. But that's an issue with PL design, not with metaprogramming.

shooting yourself in the foot is correspondingly going to become much easier

True! I won't deny that. But my position is this:

• when we need expressiveness, we'll find a way to get it, whether at development-time or at runtime
• it is easier to address issues if they are visible at development time
• it is easier to optimize and specialize code constructed at development time
• thus, it is preferable that expressiveness be achieved at development time

Shooting oneself in the foot is a possibility. Design and discipline may be necessary to avoid that, just as it would be at runtime. But it is better that we can shift potentially problematic expressions to compile time, when we're better prepared to handle being shot in the foot.

Every Turing complete programming language should support Turing complete metaprogramming. The converse is not true.

What constitutes visible progress for compilation?

If your compiler has any incremental output about what it's working on, that would be sufficient. A more advanced system might render the compilation process. And one could use static trace operations, just as one does with embedding warnings or errors.

Define 'really long': I started my carreer working on a BIG C++ project where the normal compilation time was ~6hours.

[ To add salt on the wounds: partial recompilation didn't work for several years (you had to do always make clean; make, a normal make failed), due to a compiler bug. ]

I think you're contributing to my case here.

To me, these days, 'really long' is anything more than a couple (2-5) minutes. But I rarely have patience for compiles longer than a few (2-5) seconds, so incremental compilation is very important. And in most situations I think it should just take a handful (2-5) of hundredths of a second so I can get (perceptually) instant feedback. ;)

I don't see how? A normal full compilation was 6h.
As for incremental compilation, when I found and workedaround the compiler bug, it was 30-45min: C++'s compilation with lots of (generated) class is really slow..

LtU doesn't support markdown. Use old-fashioned blockquote to do a quote.

C++ is its own kind of hell that many of us ignore as being unnatural :)

But did those compiles need to be so long? Or was this more a consequence of language choice and careless design of the dependencies? Did you even try decomposing the program into libraries, plugins, or services?

If your program took 30-45 minutes to start up, you'd find a way to fix it. But your compile-times are most likely caused by technical debt that you simply never bothered to address or thought of as 'a serious problem'. I've very often seen people take shortcuts that are syntactically convenient to the authors (like a collect-them-all header file) without due consideration of how this will inconvenience the author in other ways (like very long compile times).

Of course, our languages should make effective modularity easy for us. C++ and the typical make systems surrounding it don't qualify. You really should 'blame the tool'. Bugs occur at all layers, including logic and design. C++ has very some serious design bugs with regards to modularity, especially in the presence of templates. Similarly, make systems using timestamps instead of byte-level comparisons are poorly designed for generated code.

I haven't written a type-level program yet, but I don't see why it should be difficult to find this out.

[note: slight troll intended with title ;-)]

Fixed, thanks. The unicode conversion a few years back wasn't entirely successful.