Lambda the Ultimate

Around April 1 (but doesn't seem like a joke) 2013, on arxiv:
Alberto Carraro, Thomas Erhard, Antonino Salibra,
The stack calculus
(direct PDF link)

We introduce a functional calculus with simple syntax and operational semantics in which the calculi introduced so far in the Curry–Howard correspondence for Classical Logic can be faithfully encoded. Our calculus enjoys confluence without any restriction. Its type system enforces strong normalization of expressions and it is a sound and complete system for full implicational Classical Logic. We give a very simple denotational semantics which allows easy calculations of the interpretation of expressions.

I haven't looked at the details yet, but the result are surprisingly simple and look deeply interesting -- if you're into that sort of thing. I was always a bit rebuted the relatively large size of classical calculi, with lots of rules on top of the lambda-calculus. This one doesn't have a lambda primitive (a bit like System L in this respect) and is surprisingly concise.

(Fun fact: intuitionistic calculi are structured by the fact that there is only one hypothesis on the right of the turnstile. They have at most one hypothesis on the left of the turnstile.)

Nearly all languages with imperative elements have some kind of an array. In C
an array is just a typed pointer to a memory region. You can address the
different elements by giving an offset to the start of the memory region. The
compiler multiplies the offset with the size of the objects contained in the
array to get the actual offset in bytes.

The C view of arrays has certain advantages: It is memory efficient because it
uses just one pointer. Accessing elements is easy because it just needs some
simple address arithmetic.

But the C view has some pitfalls as well. First you might fail to allocate
memory for the array. Then the pointer to the memory region has some undefined
value. Second you might read elements of the array which have not yet been
initialized. Third you might read from or write to elements of the array which
are not within the allocated region.

Modern languages avoid this pitfalls by certain methods which can be executed
at compile time or at runtime. The failure to initialize the pointer to the
memory region is usually handled by initializing all pointers with zero. Any
access to a zero pointer results in a runtime exception. Addressing elements
outside the region is usually handled at runtime as well by storing with the
array its capacity and generating an exception if elements outside the region
are addressed.

All these solutions avoid memory corruption but they have a cost. Additional
code is required to check null pointer accesses and to check out of bound
accesses. The single pointer implementation is no longer sufficient because
the size of the allocated region has to be stored in the runtime object.

A language which allows formal verification can avoid all these pitfalls
without any cost. Without any cost? Well -- without any runtime and memory
footprint cost. But nothing is free. Some assertions must be provable at
compile time. I.e. whenever you want to access some element of the array you
have to be sure that the index is within the array bounds. And it is not
sufficient that you are sure. You have to convince the verifier of this fact.

In the article we show an array structure in our programming
language which allows us to convince the verifier that we make no illegal
accesses.

Since an array is a mutable structure we have to address the framing problem
as well. The framing problem is addressed appropriately if for any modifying
procedure it is clear not only what it does change but also what it leaves
unchanged.

A lot of effort is done currently in the verification community to address the
framing problem. Frame specifications like modify and use clauses for each
procedure, separation logic, different sophisticated heap models etc.

In the article we demonstrate that the framing problem can be solved without
all these complicated structures. It is sufficient to regard access to data
structures as functions and have a sufficient powerful function model. It is
amazing to see that proper abstraction makes some difficult seeming problems a
lot easier.

Okay, so it's Easter Sunday, and I feel a bit risen (in the sense of bread dough, that is — full of bubbles). What is more, I have finally made it through Learn You A Haskell, and in consequence I no longer fear The Monad.

Indeed, I found myself perpetrating the following little ditty, which I hereby share with other Haskell fans who are also fans of 42nd Street:

We're in the monad,
We're in the monad,
We've got a context that we have to pass along!
We're in the monad,
Our life's not so bad,
Well-typed imperative programming can't go wrong!

We never need to muta-
Te inscruta-ble state,
And when we see IO types
We can look those guys right in the eyes ...

We're in the monad
(Just rhymes with "gonad"),
Let's choose it, use it,
Keep it moving along!

Why is doing type dispatch on method calls different or more acceptable to (static) type theorists than doing type dispatch on continuation (return) calls?

Function calls and function returns are completely isomorphic, as anyone can prove by transforming a program into continuation-passing style. What possible justification then, can there be for considering type dispatch "sound" and return dispatch "unsound"?

The more I think about this the more fundamental a question it seems to become.

The essence of sound static typing is that, at any point in the program, we know exactly what type everything is, yes? Without resorting to nasty labels like type tags, for the purists. We can achieve that in the presence of polymorphic function calls by choosing at what point in the program to continue based on what type/s we are returning.

There is no difference between this technique and choosing what point in the program to call based on the argument types, because after all every function return is just a function call to a continuation. In both cases, we know exactly what type everything is at every point in the program simply because we do not go to points in the program where the types we have in hand would result in a type mismatch with the types expected at that point in the program.

Syntactically some code may look like a ladder of type checks, but the clauses can be treated as separate continuation addresses to pass to the function whose type they are checking.

I have the following ideas for function call syntax
(the function sum() gets two integers as named parameters a and b and returns int):

a) c = sum.a( 42 ).b( 42 )

b) c = sum( a:42 b:42 )

Which one would you prefer and why?
In the given language there are only named parameters, all of which are required
in the call in the order they are defined.

Lets face it: Almost all code needs to be maintained, meaning it needs to be fixed and/or extended (Except TeX, but even that needs to be ported to new languages/environments ;)). In order to be maintained, code needs to be understood. So what is the evaluation strategy that you would think is best maintainable? I vote for call-by-value.

I wonder if it makes any sense if the caller of a function decides weither a parameter is passed by reference or value. Often when I look at code (C++ mostly) I ask myself "Is this one changed by the function?" and I have to look up the function declaration. Does anyone know of a language implementing such abstraction?

Edit: I just realized, that the caller can control how an argument is passed by either making a deep copy before passing it (call-by-value) or not (call-by-ref). Only thing is, the function needs to define this argument as ref. Also this does not work well together with manual memory management, because if you create deep copies of stuff on the fly they do not get cleaned up afterwards, because the function receiving the arg does not know it has been copied before.

I am not up to it at the moment, but how about someone summarize the developments in the Javascript world (lljs, asm.js etc.) for those not following that world too closely? Thanks.

Now that we are close to releasing Mozart 2 (a complete redesign of the Mozart system), I have been thinking about how best to summarize the lessons we learned about programming paradigms in CTM. Here are five "laws" that summarize these lessons:

1. A well-designed program uses the right concepts, and the paradigm follows from the concepts that are used. [Paradigms are epiphenomena]
2. A paradigm with more concepts than another is not better or worse, just different. [Paradigm paradox]
3. Each problem has a best paradigm in which to program it; a paradigm with less concepts makes the program more complicated and a paradigm with more concepts makes reasoning more complicated. [Best paradigm principle]
4. If a program is complicated for reasons unrelated to the problem being solved, then a new concept should be added to the paradigm. [Creative extension principle]
5. A program's interface should depend only on its externally visible functionality, not on the paradigm used to implement it. [Model independence principle]

Here a "paradigm" is defined as a formal system that defines how computations are done and that leads to a set of techniques for programming and reasoning about programs. Some commonly used paradigms are called functional programming, object-oriented programming, and logic programming. The term "best paradigm" can have different meanings depending on the ultimate goal of the programming project; it usually refers to a paradigm that maximizes some combination of good properties such as clarity, provability, maintainability, efficiency, and extensibility. I am curious to see what the LtU community thinks of these laws and their formulation.

About the purpose of threads — especially green threads — I would like to hear suggestions about models, metaphors, terminology, or tactics about why this form of code organization is a good idea. A very high-level, hand-wavy perspective is what I hope to explore, to inform docs one might write for new users of code who ask simply, "But why?" If anyone wants to contribute, I'll also post short comments too, though I'm more interested in what other folks think. Note other ways of organizing code amount to the same thing, just folded differently; for example, coroutines are just green threads by another name and focus, at least in broad terms.

I've been thinking about green threads all the time lately, outside work, imagining diagrams and prose to explain the point, as starting context to motivate a library architecture whose VM model revolves around green threads (and groups of them associated under one identity in simulation of a green process). Working on solutions for a long time can make one focus too hard on the answer, and not enough on the question; so I hope I can get folks to ask rhetorical questions that amount to vague problem statement(s) causing one to seek a thread oriented design.

Ideas I had earlier this evening got profoundly vague as I tried to generalize. I suspected thread use causes hierarchy flattening, and simplifies by making many complex things uniform in organization. Another half-formed idea likened thread use to a kind of indirection, but a flat top-level indirection, with threads as equal peers. You see I'm trying to squint and find really coarse form and structure here.

Here's one last anecdote for entertainment's sake. I'm not sure what year it was — maybe 1996? — but I had a chance to ask Ike Nassi at Apple what he thought needed to be done for Dylan to gel/progress/matriculate/etc, because he was in charge of the Dylan group and I thought he might have a view from on high. He surprised me by saying he wished Dylan had defined a thread model. My first reaction was, "What does that have to do with anything?" But now I get it. So I wonder what I didn't grasp then, which I learned since, that makes the difference.