Interesting new paper from T. Sweeney and others

Formalisation of the λℵ Runtime

This is the formal details paper. The summary/rational paper is apparently due to be published by the ACM next month.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Our language has two key

Our language has two key features that combine to make it suitable for dependent typing. First, it does not have separate languages for expressions, types, kinds, and sorts, it just has a single language of terms. Second, terms specify sets of values rather than single values, as in most languages. Terms that specify singleton sets are used to specify computations, and terms that specify sets of arbitrary cardinality are used to express type information. -- Introduction
I've contemplated developing a language where types and values are the same. And recently, I have need for a good dependently typed language for modeling a heterogeneous, distributed, virtual machine. It might be worth keeping an eye on this language.

Begging forgiveness

(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

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

Proofs as Programs

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.

New paper is a much better overview

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.

Types as Multiple Values

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}.

Entangled issues

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.

type:type semantics

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.

So the verifier checks induction?

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?

Summary/rationale paper

The summary/rationale paper appears to be available here.

Thanks, I looked around but

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

Typechecking factorials

The factorial function is expressed as fact(n:int):int=if(n==0) 1 else n*fact(n-1). The syntax :t=v captures lambda-mu's "staging construct".

When the verifier verifies this code, it checks that the value v is an element of type t, and produces an error otherwise. But when the verifier or runtime execute the code, it returns a denotation saying "the result is of type t", rather than executing the value expression v, which might diverge.

This staging construct is powerful and can be extended to include a logical expression determining whether to execute the value expression: fact(n:int):int=[.if(isValue(n))] if(n==0) 1 else n*fact(n-1). In this case, the verifier can determine that fact(3)==6, and can also verify that g(x:int)=fact(x) is typesafe without looping.

This borrows from functional-logic languages. The staging construct is similar to Prolog's support for impure predicates, which control the flow of execution to prevent unnecessary divergence.

Hmmm

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.

Related: A Partial Type Checking Algorithm for Type : Type

A Partial Type Checking Algorithm for Type : Type

Inconsistent and undecidable type systems are very appealing for the unification of types, kinds and terms, but the divergence of compilation is a turn off. The above type system ensures that if type checking diverges, it's only because the computation it's checking diverges, ie. type checking terminates for all typeable terms. It's not clear whether lambda-aleph has this property.

Naive question

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

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

Isn't a really long

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

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?

Re: depends on quantity and size

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.

Isn't a really long

> Isn't a really long compilation ALWAYS a bug?

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

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 think you're

> I think you're contributing to my case here.

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

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 :)

re: long compiles in C++

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.

Adding printfs?

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 ;-)]