Lambda the Ultimate

Some of you might have followed some of my posts during 2012/2013 where I described the design of a programming language which allows static verification.

The previous working title had been "Modern Eiffel" since my first attempt had been to create a variant of Eiffel which allows static verification. During the language design more and more weaknesses of Eiffel popped up which are in the way to do static verification. The most prominent weak point is that Classical Eiffel is not type safe.

The result of my language design activities is a new language which has some syntactic resemblance to Eiffel.

However semantically the new language now called Albatross is more like Coq or Isabelle because it has a functional core and it allows to state assertions and prove them.

The last to years I have worked on a compiler and verifier for the language. The effort clearly has been underestimated by me and the one-year project has already taken two years and the available implementation has still a lot of restrictions. However the theorem prover works quite well and it certainly will take some time to complete the compiler.

For those of you who know Coq you might enjoy the capabilities of the proof engine and enjoy the fact that there is no extra proof language and all proofs are expressed by pure statements in predicate logic. Proof automation is done by predicate calculus as well and no by an integrated language like Ltac. Therefore the language is easier to learn than Coq, because every programmer has a well developed intuition about logic.

You can find the downloadable version of the compiler and a language description at the Albatross website.

[Church 1934] stated the fundamental paradox as follows:

"in the case of any system of symbolic logic, the set of all provable theorems is [computationally] enumerable... any system of symbolic logic not hopelessly inadequate ... would contain the formal theorem that this same system ... was either insufficient [theorems are not computationally enumerable] or over-sufficient [that theorems are computationally enumerable means that the system is inconsistent]...
This, of course, is a deplorable state of affairs...
Indeed, if there is no formalization of logic as a whole, then there is no exact description of what logic is, for it in the very nature of an exact description that it implies a formalization. And if there no exact description of logic, then there is no sound basis for supposing that there is such a thing as logic."

An old POPL paper from 1982:

We describe five paradigm shifts in programming language design, some old and some relatively new, namely Effect to Entity, Serial to Parallel. Partition Types to Predicate Types. Computable to Definable, and Syntactic Consistency to Semantic Consistency. We argue for the adoption of each. We exhibit a programming language, Viron, that capitalizes on these shifts.

Summaries of the shifts (from paper):

• From Effect to Entity. Large objects are made as mobile as small, so that they can be easily created, destroyed, and moved around as entities instead of being operated on piecemeal as a static collection of small objects.
• From Serial to Parallel. Constructs intended for parallel computation are also used to subsume both serial and data constructs, achieving a simplification of the control structures of the language as well as providing a framework for organizing the data structures.
• From Partition Types to Predicate Types. The partition view of types partitions the universe into blocks constituting the atomic types, so that every object has a definite type, namely the block containing it. The predicate view considers a type to be just another predicate, with no a priori notion of the type of an object.
• From Computable to Definable. Effectiveness is a traditional prerequisite for the admission of constructs to programming languages. Weakening this prerequisite to mere definability expands the language’s expressiveness thereby improving communication between programmer and computer.
• From Syntactic Consistency to Semantic Consistency. Consistency is traditionally enforced by syntactic restriction, e.g. via type structure. A recently developed alternative popularized by Dana Scott takes the dual approach of resolving inconsistencies via semantic expansion as done for models of the untyped lambda calculus. We argue that the latter approach simplifies language structure.

Nothing like that could get into POPL anymore :) What are the paradigm shifts going on today?

These last few months I have been a bit frustrated by my own relation to LtU; I wondered on a few occasions whether I should stop visiting the website frequently, and I eventually sort of decided not to. It is not easy to voice exactly what the problem is, even less easy to know what a solution could be.

I would say the observed symptom of the problem is simple: the proportion of LtU's discussion that I feel strongly interested in is decreasing. What about you?

I think decrease in interest for LtU wouldn't be a frustrating problem if there was another place to supersede it. Unfortunately, I know of no such place: the alternative that is developping right now is a balkanization in a multitude of places, many of which are closed gardens (eg. Quora) I don't wish to help grow prosperous.

(It's of course to be expected that not all LtU discussions interest everyone, as the topic is quite broad and people have different tastes about different subdomains.)

Why am I less interested in LtU discussions? I think there has been at times a better balance between technical discussion around articles (articles mostly following the standards of academic presentation) and less-focused discussion, possibly more radical but less precise viewpoints.

I don't think there are more less-focused / off-original-topic discussion than before, or too much of them, but rather that there not enough of the more structured technical comments. In particular, I mean no criticism of the current LtU members or discussions, which bring many interesting point of views -- there might be things to improve in this area, but I don't think that is where the real gains are. I would be more interested in attracting more "research discussions" but I don't know how to do it.

On the positive sides, here are three examples of interactions that I personally enjoyed a lot recently, and would by themselves justify my continued LtU activity this year:

• Tom Primožič linked the draft version of Andreas Rossberg "amazing" 1ML paper; without this link, I probably wouldn't have learned about this exciting work for a few months.
• Sean McDirmid posted article versions of his work on type inference (and previously, Glitch), that helped make more precise interesting discussions that had been going on and off on LtU for a long time.
• Robert Atkey saw an on-the-side remark inside the LtU submission on the very interesting work on incremental computation, and gave it enough thought to produce an amazing blog post -- that I'm sure will bear further fruits.

(That's of course not the only things I liked on LtU recently. There are many things I come to know through LtU that I wouldn't otherwise learn about, typically on approaches to programming languages that are closer to social sciences (user psychology and experimental studies, sociology of adoption, etc.)

What were your own "value moments" on LtU lately?

I've stumbled across something in my compiler work and wondered if anyone has run into anything similar, or knows of any existing literature about it.

The problem I'm working on is dealing with the template bloat problem in an AOT language, without resorting to type erasure. I know that there are some compilers which, during the code generation phase, will merge functions and data structures which have identical machine representations, but I'm attempting to do this in a more formal and abstract way, and at an earlier stage of compilation.

In mathematics, a differential is a description of how the output of a function varies with respect to a parameter. In my scheme, a "type differential" is a description of how the meaning, behavior, and machine representation of a function changes with respect to changes in a template parameter. An analysis of the expression tree for a function yields a set of these differentials. Once you know all of the differentials for a function, you can then easily compute whether any of the template arguments can be weakened, creating a more generalized version of the function that has the same meaning.

A trivial example is the "CallingConvention" differential. Let's say we have a generic function F which has a generic type parameter T, and which takes a function argument also of type T. Different values of T will have different machine representations, which changes the function signature - however, many different types have identical machine representations, so the set of possible machine representations is much smaller. On the other hand, if we change the type of the parameter from T to ArrayList[T], things are a little different - since ArrayList is a reference type, it's always passed as a pointer, so the value of T no longer has any effect on the function signature at the machine level. So CallConv[List[T] == CallConv[Object].

Other examples of type differential objects include LocalVariable, InstanceOfTest, InstanceMethodCall, FieldOffset, and so on. In some cases, the presence of a differential can be used to decide whether the compiled code should contain a static reference to a type identifier, or whether the type identifier should be passed at runtime as a hidden field or parameter.

Java's type erasure can be thought of as a system in which the set of type differentials for all functions is the empty set.

Now, what's interesting about this is that I realized that there's a kind of algebra of differentials: There are operators that can be used to sum and compose them. For example, if I have a composition of two templates, it's possible to compute the differential of the result directly by composing the differentials of the individual pieces.

Anyway, I'm sure that there's probably some pre-existing term for this - which I'd be able to search for if I knew what to name it.

The Programming Language Wars: Questions and Responsibilities for the Programming Language Community by Andreas Stefik & Stefan Hanenberg

video of presentation @ CodeMesh 2014
slides in PDF format
the paper in pdf

A presentation of the results of a number of randomized controlled trial studies of the affects programming language designs on users.

He spends a great deal of time on the need for the programming language creation community to do more of these kinds of trials and why he thinks they are so necessary.
He also spends some time defending the expected attacks that either their goal is either one language for all or a different language for everyone, both of which seemed like odd accusations to me.

Among the conclusions are

• On average, static typing improves developer productivity under a wide variety of conditions
• Threads, compared to software transactional memory, leads to approximately 8-fold more bugs among those in the sample
• Some languages (e.g., Perl, Java) have symbols so poorly chosen that a randomly generated language is just as easy for a novice to initially use
• Overall, measurements of the impact of Aspect Oriented Programming appeared to be limited and most useful in simple situations like logging
• C style syntax hurts comprehension compared to alternatives

He says that languages shouldn't be created or changed without this kind of research to back up the ideas.

Only half the interesting detail is in the slides.

questions start @ 34:00

the Perl vs java research wave previously discussed as Perl vs. Random Syntax here on LTU

Types are fundamental to both logic and computation:
* Types are fundamental to avoiding contradictions in logic. For example, proper use of types avoids all the known paradoxes. See Types in logic.
* Types are fundamental to computation. For example, in the Actor Model it is necessary to know the type of Actor in order to send it a message. See Types in computation.

The issue of types arose in another LtU discussion where it seemed tangential but since the topic is fundamental, it is worthy of discussion because there seems to be a great deal of confusion and controversy on the part of both theoreticians and practitioners.

Our programming tools should be more democratic, egalitarian, said (Dr.? Mr.? I was assuming Dr.) Edwards a while back. (I, a peon, have great respect for and mostly agree with him, of course, utterly seriously.)

What I see happen in the real world is something like: (1) hack something up to get it working asap; (2) oh no we got actual customers [remember the famous quote about not being able to change Makefile syntax?] we'd better keep on truckin' with this since they want new features and are already bought in to how it works today; (3) who the hell wrote this crap, I can't possibly maintain it! [remember the famous death of Netscape?]

So if we hand people Visual Basic, they might make something great that would never have existed before. BUT what kind of rats nest of hell code will they produce, and what zillions of crazy bugs will they have, and and and.

If that is a real problem somewhere in the world sometimes, how best to address it? Rewrite it? Outsource/offshore rewriting it? Sell it to CA, Inc.?

Or something else? What could we have in our programming languages and ecosystems that would let the masses have their cake and eat it, too?

Ignorant question: Might anybody be able to succinctly say where we are vis-a-vie effects-continuations-monads? Do we have languages where we can have fun managing effects? Did we give up on the monadic approaches to this? I am too completely out of my depth / behind the times in terms of this research. As a Joe Programmer in the Street, I just want it now and in a usable fashion :-)

E.g. many years back, Filinksi's thesis seemed to talk about a nice way to get all this via monads in standard ML.

Many computational effects, such as exceptions, state, or nondeterminism, can be conveniently specified in terms of monads. We investigate a technique for uniformly adding arbitrary such effects to ML-like languages, without requiring any structural changes to the programs themselves.

Did that turn out to not have good usability or something? I have been trying to skim things related / citing that stuff, but it is all over my head at this point. And I don't yet see if/how/when any such things are reified in a language I can use.

thank you.

Based on Engelbart's famous "mother of all demos" in 1968 that showed off multiple input and output technologies, what could a MOD for PL look like today? Did we already see one with Bret Victor's work, or do we need something more?