Haskell is a dialect Algol!

Modernized Algol (MA) - revised by Robert HarperPermalink

MA = PCF with a modality$modality$ - distinguishes expressions from commands

a$a$’s are assignables not variables! x$x$’s are variables! Assignables are not a form of an expression of it’s type. Assignables is a location in memory whose contents has a type, where we write a1∼τ1$a_1\sim {\tau }_1$ (not a1:τ1$a_1:{\tau }_1$). Assignables are really indices to a family of get$get$, set$set$ operations, they are not values, arguments, or evaluated. They are just indices, and get$get$’s and set$set$’s are just capabilities to get and set a$a$. We can define references, i.e. &a in a real programming language, as a pair <geta,seta>$<ge{t}_a,se{t}_a>$, which just a thing that gives you access to the capabilities of getting and setting a$a$.

Types and expressions are “pure” - don’t depend on memory, whereas commands are “impure”.

StaticsPermalink

where Σ$\Sigma$ is tye types of assignables, i.e. a1∼τ1,…,an∼τn$a_1\sim {\tau }_1,\dots ,a_n\sim {\tau }_n$.

It means a well-formed command whose return values has type τ$\tau$

The above is the Introduction rule for cmd

The above is the Elimination rule for cmd

It means I am declaring an assignable: I declare a, initialize it to e, and run the command m′. A type is mobile if the value of the type can be pulled out from the scope of the assignable. Example of mobile types: eager natural numbers, pairs/sums of mobile types. Example of not mobile types: functions (because the body of the function can use assignables even if the ultimate return value is nat), commands. This will be explained in later sections when we talk about the dynamics.

Exercise: We have the following [Pre-]monad defined:

Show that you can define r and b for T(a)=cmd(a).

The important fact is that you start with the modality, then they can be formed into a pre-monad.

DynamicsPermalink

μ||m means a command m in memory μ. The notation is designed to connecto with concurrency. The idea is that we have a concurrent composition of a main program m running simultaneously with threads that govern the contents of each of the location.

Exercise: define set

We have something called Stack Discipline invented by Dijkstra. The idea is that the assignables in Algol are stack alocated. When I do a dcl(e,a.m′), I declare an assignable in m′, I can get it and set it in m′. When m′ is finished it’s deallocated.

To rephrase the above in English: Start from lower left: I have a value e which is the initializer of the assignable a and I want to execute m in the presence of that assignable. What can I do? I go above the line and do: let’s extend the memory μ with a having the content e, and I execute m, and I will, in the process of doing that, maybe modify some outer assignables (turn μ to μ′), maybe modify some inner assignables (make a have the content e′ instead of e originally) and get a new command m′. Then I update the memory (from μ to μ′), and reset the world (from m to m′). In other words, I take the starting state where I declare a being initialized to e and execute m, once you take a step of execution of m in the situation of μ⊗a↪e, you might have done a set in a and updated that to e′! The resulting state is: I restart your program in the situation in which the initializer is not what it was (e) but what it becomes as result of the execution step (e′) and then proceed from there.

To rephrase the above in English: Start from lower left: I declare an assignable a and assign it to e, and I am returning a value ret(e′), what do I do next? The idea of the stack discipline is: when you finish executing the body of dcl then you get out of it!

Some issues with type safetyPermalink

In the above formula, in the lower left part, if e has type τ, then e′ has type τ′ in the context of Σ,a∼τ, but in the lower right part, e′ should also have type τ′, but with only Σ alone. In traditional Algol, we can only return nat, which means if a numeric value val type checks with an assignable present (Σ,a∼τ), it will type checks with the assignable absence (only Σ), only under some conditions!

So here is the question: Under what condition is the following statement true?

If e is a value of type nat and type checks with the assignable a, it will also type check in type nat without a.

Answer: Only if the successors are valued eagerly! if the successors are lazy, then the arguments of the successors are unevaluated expressions (they are no longer values val)! Algol only makes sense if the constructors of the successors are eager!

Here is an (clever) example of a successor of N doesn’t type check if lazy. I want a successor of something, which is an expression, that uses an assignable a. The goal is it will not type check outside of scope of a:

Explanation: We have a constant function that takes in a nat and return 0 z. And to type check the argument cmd(get([a])) we have to eventually type check a, even though it doesn’t matter the ultimate return value of the function because it’s constant!

This is a perfect example of the interactions between language features. We might think that whatever I do with the PCF level whatever we don’t care lazy or eager and the command level is separated. This is wrong! The hard part of a language design is to make everything fit in a coherent way. This is way language design is hard!

So traditional Algol they make things work by restricting the return value only nat, and make nat eager. A better idea is that we can demand the result type of dcl mobile! And we also need to restrict that we cannot assign values that aren’t mobile, because we can assign the value from a return value. This is the explanation of the above “This will be explained in later sections”.

MA - Scoped AssignablesPermalink

ReferencesPermalink

We can define ref(τ) (immobile) as we mentioned briefly before in the following ways:

Concretely:

Where cmd(τ) is just the getter and τ→cmd(τ) is the setter.

Then we can have:

The problem is, if you look at the type ref(τ), it only says it has getter and setters, but it doesn’t say the getter and setter are for the same assignable! So you can have a getter for a and a setter for b and you won’t know the difference. So then we can define it in another way:

Abstractly:

The type is still ref(τ), but we have the following elim rules:

MA - (Scope) Free AssignablesPermalink

All types are mobile. Previously because the stack discipline is causing us trouble about mobility, and we go back to to add some mobility rules in the statics. But there are other ways to fix this: let’s change the statics, make every type mobile, and we’ll make our dynamics fit that. Here are the new dynamics. (Also called scope-free dynamics, or in other words, assignables are heap allocated.)

Note the above transition is unlabelled.

PCF (FPC with recursive types rec) + commands above with free assignables ≈ Haskell :)

IssuesPermalink

In Algol, we have a clear distinction between expressions and commands; they are completely separated. There are many benefits of doing that. But in the “real world”, in doing that, we lose a lot of benign effects. For example efficiency, we lose:

• laziness/memoization
• splay trees - self-adjusting data structures
• …

While we are condemning benign effects, we do rely on them in real life.