I decided to take a different tack on my OBT submission. The new submission is at https://docs.google.com/document/d/1PQSc0UEHcYrfbiv_AGDxc8Wvjiy75UsyA5pM2mqRiyk/edit?usp=sharing, and also pasted below. And the pdf I actually submitted is https://drive.google.com/file/d/0B9G51OQiN3RuanMxTkFjT1pCRnM/view?usp=sharing. See you in Paris. Feel free to lobby the conference committee if you know them :-).

[updated]

The case for Algol2020

Robert Smart

There are many reasons why now is a good time for a new version of Algol, and since “we can see clearly now” it would be a shame to miss the opportunity for Algol2020.

Programming has got past the OO fever, and established a good, though still improving, feel for programming with values rather than variables. Algol68 had already made great progress in the latter direction with its fundamental principle that identifiers stand for constants.

Algol68 was a difficult language to use, and with 20-20 hindsight we can now understand why:

• The dual use of ref types for pointers and for variables was a mistake. It is true that both have the same implementation as an address in memory, but for variables we want a dereferencing coercion to operate and for pointers we don’t. Indeed, more generally, we want types to be defined by their semantics and not their implementation.
• Procedure values lacked power because they weren’t closures. This was a pity because the Algol68 rule that identifiers stand for constants is exactly what is needed to give closures a clear cut meaning.

It was a nice move towards functional programming that Algol68 had array X which was constant and behaved just like procedures Index=>X. But why then isn’t a normal mutable array an array(ref X)? Semantically you give it an index and get back a mutable value you can assign to. Instead Algol68 had a hack where a ref (array X) could be indexed and gave back a ref X, allowing one to change a part of the ostensibly constant array X value. Presumably this was intended to be more efficient, yet this is once again mixing semantics with implementation. An array(ref X) could conceivably have pointers to variables arbitrarily arranged in memory. However a simple start address and length could be a separate implementation that gives the required efficiency.

Similarly int64 can be an efficient implementation of a full int type, as long as we detect overflow and transition when necessary to a wider implementation such as BigInt.

Algol is naturally oriented to arrays rather than lists. However this is a distinction without a difference once types are oriented to semantics rather than implementation. Both lists and 1-dimensional arrays are just different implementations of what mathematicians call a “word”. This is hard to see because we are used to arrays of variables (array(ref X)) implemented by a start address and length, and you can’t prepend a new variable to that and retain the “start address and length” implementation. We can do it if we move to a fully general array(ref X), or preferably something in between. This is like moving from Int64 to BigInt when necessary.

The Wombat programming language

The Wombat programming language has been under development for 35 years (under various names) inspired initially by the desire to address the problems in Algol68 mentioned above. It has quite a lot of ideas that I would be keen to put before the Algol committee (IFIP WG 2.1), should they be interested in defining a new Algol. I list some of them here because they show what can be done within the Algol tradition.

• Behaviours are like Haskell type classes, listing properties and laws. This is similar to interface/trait without allowing them to be used as if they were types.
• It is natural to organise types in an embedding hierarchy. An Int is a Rational, and a Dog is a Mammal. This is done with apply/unapply pairs of functions (in Scala terminology). The hierarchy forms a bounded order lattice and this is the natural setting for Algol68-style Union. (Unrelatedly, we also need DisjointUnion which the application programmer will more normally use.)
• The type at the bottom of our hierarchy has no elements. It is Empty in Wombat.
• Automatic conversions and casts within the hierarchy go down to the intersection of source and destination, then up. When the intersection is Empty then other coercions, such as dereferencing, can occur.
• Diamond ambiguity (choice of conversion paths) is addressed in Wombat by combining procedures so that the fact that the two paths give the same result is checked at run time. Combinable is a weakened Distinguishable that is sufficient for some uses. Combining is also used to support procedure declaration by multiple declarations with different parameter patterns.
• The Algol68 declaration, such as “int five = 5” can, in modern style, be sensibly reduced to “five = 5”. It is natural then to allow the left side to pattern match and unpack structures. However we can have names on the left already declared from an outer level which are just representing their outer value. Wombat avoids any ambiguity by marking new names with a preceding backquote. It also extends the meaning of “=” to general unification. The benefit of this is that the same code can, in logic programming style, be declarative and can be run forwards or backwards in some circumstances.
• Wombat has an Atom type, with values being an identifier with a leading dot (.), and no Behaviours except Distinguishable. So s.length is just a procedure call with Atom parameter .length. All values are allowed to behave as procedures in a type-specific way, so the convenience of OO method call syntax is delivered with simple procedure call semantics. So if s has type String then s behaves as (String.asProc s).
• The advantages of lazy evaluation can be substantially realised by use of streams [Stream(X) = Unit=>(X*Stream(X))], and similar types, if they can be implemented in iterator style.
• We can see that proofs are going to become an important part of programming. In Wombat it is expected that when the properties and laws of a type are defined using the properties and laws of an implementation type, then that should be proved. When a specialization is added to a procedure for some implementation of the input, then it should be proved that it actually does implement the same algorithm. Inverse pairs arise in several circumstances, and it is reasonable to expect a proof that they are inverses. And so on. This is an important but new and difficult area that might make it hard to hit the 2020 date.

Naturally there are many other researchers and developers who will want to add great ideas to a new Algol.

More information about Wombat is available on the blog wombatlang.blogspot.com. The posts are of varied quality and varied relevance to the current design. The post Rationale of the Wombat Type System is an alternative OBT submission that I prepared and is perhaps a good introduction. The outline doc, "Outline of the Wombat Programming Language", is reasonably up to date, but not currently very well organised.

Rationale of the Wombat Type System

I wrote a submission for "Off the Beaten Track" (http://popl17.sigplan.org/track/OBT-2017#About). Then I noticed that it has to be 2 pages, so back to the drawing board. Anyway its at

https://docs.google.com/document/d/1R_wAxvFU9VEwUSNuawqQM9KQhVYXPSrjS-jk4wDog84/edit?usp=sharing and also appended below. Comments welcome.

Rationale of the Wombat Type System

The features of the type system that will be covered here are:

• Support embedding (lossless type conversion) and distinguish it from lossy conversions.
• Characterise types by their properties, allowing multiple implementations with differing performance characteristics.
• Allow incomplete implementations (such as Int64 for Int).

Wombat Introduction

Before getting to the subject of the talk, some aspects of Wombat need to be introduced. Yes they could be done differently, but I find that they fit comfortably with the type system features.

The following expressions are key:

• expression:type returns a value of the given type, failing if that is not possible;
• expression1 = expression2 is a unification, filling in holes on either side to make the equality true in a unique way, or failing if that is not possible.

In both cases the failure is informational not fatal, and is commonly used for flow control.

Blocks of code are just closures with Unit input. So it was desirable to have a syntax for closures that was terse when the parameter was not mentioned. A closure is just an expression in braces (such a {1+2}). The input parameter is $, and good practice is to start the closure with an unpacking unification and never mention $ again:

{ $=Complex(`re,`im); Complex(re,-im)}

Identifiers are preceded with a backquote when introduced for the first time. Operations that create structures (such as the Complex constructor here) can take holes as parameters, which are quickly resolved in this case.

There is a caseP procedure. The case operator is identical apart from a more familiar syntax. The (curried) parameters are a list of procedures, and a parameter. The parameter is passed to all the procedures, conceptually in parallel, and it is expected that all but one will fail, and the result of the one that succeeds is returned. Effectively the guards of the case statement are moved inside the alternative procedures where they just become normal statements. However more than one of the procedures can succeed if they return the same answer.

`abs = {$=`x; caseP [
                { x >=? 0; x } # ? turns bool operator to unit/fail
                { x <=? 0; -x } ] () ;

If the returned results are not Distinguishable then they are combined if they conformTo Combinable. In particular procedures are combined by using the curried caseP procedure with the list of returned procedures as the parameter. This defers the equality check and also allows the operation to be spread over multiple procedures. Procedure combining in this way is a recurring requirement.

Atom constants start with a dot (.). All values can act as procedures. So s.length is just calling s with Atom parameter .length. If s:String then this is (String.asProc s).length.

Type Embedding

In some languages we have to say “I’m sorry, you’re a Dog, you can’t also be a Mammal. However I have this irreversible conversion you might consider.” or “I’m sorry, you’re an Int, you can’t also be a Rational.” In Wombat we allow embedding with the isA declaration:

Int isA Rational by { Rational($:Int,1) } inverse
                   { $=`r:Rational; r.denominator=1; r.numerator}

The inverse operator creates an inverse pair of procedures. The first always succeeds (converting the input type up), while the second may fail. Explicitly:

(F inverse G):InversePair X Y

means that F:X=>Y is total, G(F(x:X))=x always, and F(G(y:Y))=y whenever G:Y=>X succeeds.

As we go up the hierarchy we expect to lose properties and not gain any. So the above isA declaration has the effect that Int acquires all the properties of Rational, such as the .denominator procedure. This means that no explicit conversion is necessary to convert upwards: just use the properties of that higher type as if the value was of that type, because it is. As we go up we also need more data such as the denominator for a Rational, or dog-specific data for a Mammal.

Downward and sideways conversion only happens in the presence of an explicit colon operator conversion or converting a parameter to the domain type of a procedure.

For an example of sideways conversion, suppose we have types Mammal and Quadruped, with some obvious lower types. Then someMammal:Quadruped will convert to Quadruped type and fail if someMammal is one of those pesky bipedal mammals. The rule is that we first convert down to the intersection of the origin and destination types, then up to the destination.

There is also lossy conversion established with the convertsTo operator. This only comes into play when the source and destination have Empty intersection in the isA hierarchy, in which case it acts the same as a downwards conversion. For example, the type of variable X is Assignable(X), which convertsTo X. So if we give an Assignable(Int) where a Rational is required then we convert down to Int then up to Rational. There is, naturally, no route either way between Assignable(Int) and Assignable(Rational).

Whether going up or down there is the potential for diamond ambiguity. For example suppose Int isA Rational, Int isA ComplexInt, Rational isA ComplexRational, ComplexInt isA ComplexRational. There are two ways to convert from Int to ComplexRational. This is solved by combining the procedures using caseP.

It's Types all the way down

Wombat has Behaviours (spelt with or without the 'u’), which are much the same as Haskell type classes. A type is defined by its compliance with a particular Behaviour. A type can also be declared to conform to other Behaviours, and can do so in more than one way (controlled by a 'how’ parameter which is often specifiable as an optional operator subscript).

We might declare Nat by having a zero, successor and ordering with appropriate laws. That doesn't generate any implementation. Instead every non-primitive type has to have one or more implementations using some other type. Nat might reasonably be implemented by BigUInt, with Nat’s operations implemented using BigUInt’s operations, and its laws proved using BigUInt’s laws.

Ultimately this has to lead to primitive types. These have a Behaviour with operations and laws determined by the specification of the compiler target, and they are the only types that exist at run time.

Yes we can:

• fully define Nat with a few simple operations;
• code all other operations, such as add, using those simple operations;
• implement those simple operations in BigUInt.

But that is going to be a very inefficient use of BigUInt. The rule is that a use of a type is not allowed to peek inside at the implementation. It is only allowed to use the type’s defining Behaviour. The exception is “addSpecialization” which can add a specialization to any procedure, replacing a value of a type with some implementation of that type. The thing that makes that safe is that the programmer is required to provide a proof that it is an accurate specialization. Unfortunately the details of that are not worked out, and the only proof in the initial design is TBS, which always works. Here is some out of context code:

`np=Nat.property;

  Nat conformsTo Monoid name .additive by # Monoid extends Distinguishable
      [
          .zero -> np.zero # monoid .zero goes to Nat .zero
          .binop -> `add={$=`x,`y;
                          `up,`down=np.succ; # .succ is an inverse pair
                          caseP [{y=np.zero; x} # note: down fails for zero
                                 {add(up x, down y)}] ()
                         } # need to add implementation specializations!!
      ];
  Nat.behaviour(Monoid).additive.binop addSpecialization BigUInt.add
      covering (Nat as .bigUInt)*(Nat as .bigUInt)=>(Nat as .bigUInt)
      proof TBS;

Implementations are interlinked by inverse pairs of total procedures. All implementations except one have to link to one of the others. But we also allow partial implementations which must link up to a wider implementation (usually to a full one) with an InversePair of procedures that can fail going back down. For example Int64 is an important partial implementation of Int for some target hardware. However operations producing Int64 must detect failure, leading to rerunning the failed operation to produce a BigInt and to following a different continuation of the code from that point.

Every subtype automatically becomes a partial implementation of the higher type. So Int is a partial implementation of Rational and we can add a specialization for, say, .denominator that always returns 1.