Combining procedures in Wombat

The need to combine procedures occurs a few times in the Wombat design. It is something that forced itself on me, and I'm surprised it isn't a common feature of programming languages.

The most obvious example is the case statement. In Wombat the conditions which select the operation are not separated. Instead there is just a list of procedures which contain the tests inside them, and fail harmlessly (Fail.next) when the condition is not met. So in case it is normally expected that exactly one of the procedures will succeed, and the result of that procedure is the result of the case statement. There is also a firstCase statement that tries the procedures sequentially till one succeeds, but in case the procedures are executed in parallel (conceptually).

The corresponding caseP procedure is curried and with the parameters reversed, so it has type

List(X->Y) -> X -> Y

All the procedures in the list are passed the X parameter and evaluated in parallel. Normally all except one of the procedures fails harmlessly (Fail.next). It is also permitted for more than one to  complete as long as they all return the same value. Note that for these purposes they might be different types connected by an isA relationship. For example Int isA Rational, so it is ok if one procedure returns 2 and the other returns Rational(2,1).

If the results of the multiple successful procedures are not equal then they can be combined in a way that ensures their compatibility at the later point of use (if their types support that). In particular if more than one procedure is returned then the result of the caseP is a procedure which, when later executed, will evaluate all procedures and:

• If all but one fail harmlessly then return the result of that one;
• If more than one returns then they need to agree on the result;
• Except that it is also permissible to combine the results if procedures are returned.

So, neatly, the way procedures are combined is with the caseP procedure.

We've glossed over a couple of things. During the parallel evaluation of procedures it is permitted for there to be side effects as long as they all have exactly the same side effects in the same order, in which case that side effect happens just once. Also what if the result is a structure that contains some procedures? Then the structure must be the same with the corresponding values the same or, if procedure values, combined.

[see also: http://wombatlang.blogspot.com.au/2015/09/on-infinite-things.html]

More rambling on Types

What is the difference between static and dynamic typing? In real life they blend into each other, which is why we see the big interest in gradual typing.

At one extreme we have the idea that "the Type is everything known about the value of an expression". In this space we have static typing if the compiler knows as much about the value of the expression as the programmer. Now the programmer is likely to know quite a lot about every expression in the program, and how it relates to other expressions. The compiler will certainly generate better code and give better error messages if it knows all that stuff too. But it is a bit unrealistic. In Wombat the programmer can put in as many or as few failure-inducing tests as he likes, and these potentially give information to the compiler to use.

At the other extreme we have the view that "a Type is constructed (and deconstructed) using a set of operations provided by the programming language". In such a static typing environment then the Type (in that sense) is always known at compile time. I would add that statically typed software is then expected to be written in such a way that it assumes no additional knowledge about values beyond the Type. It is certainly part of the plan that Wombat's general purpose libraries can be written this way, but I don't think it is practical to write many actual specific programs in that style.

In this latter view of the world the thing that makes a program dynamically typed is that the same expression can have different Types during different passes through the same section of code. This certainly seems undesirable. However this is something that always happens in languages with subtyping like OO languages and Wombat. A variable myMammal might be a Dog sometimes and a Cat at others, but it is always a Mammal. In Wombat this is taken to extremes so that every value belongs to a whole lattice (http://en.wikipedia.org/wiki/Lattice_%28order%29) of types, with Any at the top and the subset type that contains only itself at the bottom.

Use and meaning of Types

Before my simplistic take on Types, here is some history:

Types in programming languages come at us from two very different directions: the brutal reality of programming physical computers; and the rarefied realm of the foundations of Mathematics (starting with Bertrand Russell's theory of Types). Not surprisingly the collision of the two currently taking place in modern programming languages is not a very comfortable event.

In the beginning of programming (Assembly language, BCPL) there were groups of bits, and the programmer needed to know what they meant so that sensible things happened. But there was nothing to stop you doing floating point adds on integers, or using 0 (or other integers) as memory addresses. Then languages gradually added types to avoid simple errors and facilitate conversions. Algol68 nearly got it right, but 2 big errors (no closures and combining pointers and variables) led to a general loss of interest in getting it right. This led to brilliant but hacky languages: C, C++, Java, Python, and more.

Meanwhile the Mathematicians struggled to understand various sorts of logic and associated Type theories. There were various attempts to build programming languages on these ideas leading to current languages such as Haskell and ML. Then came software to support the development and verification of mathematical proofs. These turned out to be similar to programming languages. There was also an increasing need to prove the correctness of programs. So this was a natural way for Types from the mathematical side to force their way into real world programming. Very recently we see the creation of Homotopy Type Theory (HoTT) which seems to bring the automation of mathematical proof and the verification of software a lot closer.

Wombat comes very much from the practical programming side. It can be seen as an effort to fix Algol68 and add some modern things. I am struggling to understand the Mathematical side of Type Theory, because it is particularly important to incorporate proofs of correctness to Wombat. I'm quietly confident (hopeful) that Type Theory types can be expressed correctly using Wombat's types.

A traditional view (e.g. in C) is that Types describe how data is laid out in memory. This goes along with the pre-functional style of programming where all names are variables (leading to the extreme position in Java and many other languages where the poor programmer has to deal with mutable pointers to blobs full of more mutables). This then leads into the quagmire of distinctions between value types and reference types.

A functional-oriented approach is to view types as the string of bits that get put on the stack when a value of the type is being passed to a procedure (assuming a completely unoptimized execution model), plus a collection of primitive operations for that type which programmer and compiler need to keep in mind. This is where Wombat plans to be for primitive types, except that there are also axioms for those primitive operations. The actual types that a programmer is more likely to use in Wombat are defined by their operations and associated laws (which are proved true from the Implementation type's operations and laws which are axioms).

Only primitive types remain at run time, which is not to say that values of those types are actually computed. For example we create a mutable (=assignable) Int64 on the stack by:

`x = loc Int64 ()

But the resulting memory address is a fixed distance from the frame pointer and we expect the compiler to just take a note of that and generate the address on the fly whenever necessary.

However the idea of types that really motivates a lot of Wombat is this:

The type of an expression is just everything the compiler knows about it.

This lets us look at a program upside down. The natural view is that during execution of the program, expressions take on values which become grist for the mill of other expressions. The upside down view is this:

• We start by building the program's abstract syntax tree (AST), and then execute that symbolically to create what we might call an Abstract Execution Tree (AET). 
• The AET cannot follow recursive calls too far or it will be infinite. It has to be lazy from some depth. Or maybe every optional bit that might never be executed is lazy.
• We work out everything that can be worked out before any execution takes place. At this point the program can't make further progress till it runs and interacts with the outside world.
• Initially and then between each interaction we evaluate expressions. Each expression we evaluate must narrow the range of possible values of some other expression: otherwise there was no point in evaluating it and the evaluation engine shouldn't have done so.

So instead of the compiler generating code to execute the program, it generates code to do optimal JIT specialization of the whole program. The final specialization completes program execution. One fondly imagines that this process can be highly parallel.

This view of types blurs the distinction between static and dynamic typing. Indeed it is somewhat inspired by Yin Wang's essays on this. Sadly he seems to decide that his old essays aren't quite right and deletes them.

The Lean Theorem Prover

It is an exciting time at the crossroads of Mathematics and Programming. The Lean Theorem Prover (http://leanprover.github.io/) looks very useable for what Wombat needs. To quote from an earlier post (Whither Wombat):

More substantively is the issue of the status of laws/axioms. It used to be that these were just comments. Then languages started including them in an executable form, with a bit of handwaving “quickcheck style checking programs might use this”. That’s where Wombat came in, and the way it is specified in the doc.

But I don’t think this phase will last long. It is time to do it properly and prove all claimed properties:

• Primitive types will come with axioms describing their behaviour, from the X86/JVM/whatever manual.
• The semantics of other Types will be proved from the code implementing the semantics using the assumed (if primitive) or proved (if not) semantics of the implementation.
• Other things that need to be proved include:
• proving that a supplied specialization does indeed implement the same algorithm as the original;
• proving that the procedures linking one implementation to/from a more comprehensive one (usual the main one) are inverses (where the reverse is defined).
• …

The hope, with respect to Lean, is that the Wombat compiler will be able to call the Lean API to perform these proofs. In many cases one would hope that Lean will just work out the proof itself. If not one would hope that the programmer can use the Lean interactive mode to construct a proof which can be included in the program. I suspect this is all a bit ahead of its time, but it would certainly be interesting to try to get it going in a small subset of Wombat.

Wombat hibernating

My reader(s) have probably noticed that not much is happening. This is not likely to change for a little while.

I look at new programming language stuff for signs that anyone might have looked at Wombat. In Odersky's latest talk (http://www.slideshare.net/Odersky/scala-days-san-francisco-45917092) he postulates union and intersection types which seem a bit Wombaty.

I always think that Implicits should be important in any language, as they are in human languages. To date I've assumed that this can be handled in Wombat with default parameters and with optional inner suboperators within operators. I should look at the improvements Scala in introducing and think about that.

I also thought Jon Pretty's slides on exceptions were interesting: http://rapture.io/talks/exceptions/sanfrancisco.html.

Wombat Type Hierarchy

It is natural to regard some types as being contained in others. An Integer is a Rational. A Dog or a Cat is a Mammal or a Quadruped. Programmers expect this to mean that they can use an Integer where a Rational is expected, and so on. If you follow this through to its logical conclusion you are bound to get the Wombat solution outlined below, or something very close. Note that this is about lossless conversion which can be reversed in a “case” statement. Wombat also allows for lossy conversion with convertsTo which will be covered in a separate post.

The relationship between types is declared (and tested) with variants of the “isA” operator. When declaring that Int isA Rational we provide a pair of functions:

1. The “to” function creates a Rational with denominator 1;
2. The “from” function fails if the denominator is not 1, else returns the numerator.

The effect of declaring Int isA Rational is that Int acquires all the semantics of Rationals. For example if r:Rational then we can get the denominator as r.denominator. This must now apply to Ints as well. By default the Int value will be converted to Rational, then the denominator will be extracted. It is possible and easy to add a specialization so that for Int values it returns 1 directly, though it seems unlikely that it would get much use.

Also, all overlapping semantics (such as, in this case, addition and multiplication) have to be compatible. This is a delicate matter, particularly if the types come from modules from different sources, so we’ll defer it to a later post.

Another motivating example would be similar to OO style subtyping. Suppose we have types Mammal, Quadruped, Cat and Dog such that Cat isA Mammal; Dog isA Mammal; Cat isA Quadruped; Dog isA Quadruped. Now what can we make of this list:

[ myDog myCat anotherDog ]

What is it a list of? It could be a list of Mammals, or a list of Quadrupeds. Should we make the programmer decide? What if he wants to pass this to a procedure that expects a list of Mammals, but later wants to pass it to a procedure that expects a list of Quadrupeds? It is stuff like this that drives people away from static typing to dynamic typing.

In Wombat: for every set of Types there is a Union which is the smallest Type that is above all of them. So our list above is a list of Union(Dog,Cat). This automatically behaves correctly with respect to declared relations. So Union(Dog,Cat) isA Mammal and Union(Dog,Cat) isA Quadruped. Note that all the semantics of Mammal and of Quadruped are also compatibly in Dog and Cat. So there is no problem bestowing them on Union(Dog,Cat). In a Union where the components have no common higher isA relation defined, such as Union(Dog,Int), then there are no defined semantics other than those from Union.

To fill out our list example we need to have a rule that whenever X isA Y then List(X) isA List(Y). Which gets into yet more delicate areas that we’ll leave for another day.

On the other side we have Intersection(Mammal,Quadruped) which is the largest type that is below each of them, and gets rid of those pesky bipedal mammals. There has to be at least one type that is declared to be below all the types in the Intersection, otherwise the Intersection is Empty.

The rules for the interaction between Union and Intersection need to be extended in obvious ways (such as associativity) and this makes Types into a lattice (http://en.wikipedia.org/wiki/Lattice_(order)).

Wombat’s type-assertion/conversion operator is “:”, and it can go up or down or even sideways. So myDog:Mammal always succeeds (calling the “to” conversion), myMammal:Dog calls the “from” conversion and may fail (allowing other options to be tried in a case statement). Finally myMammal:Quadruped will go down to the Intersection (possibly failing in the bipedal case) then up. Only when the Intersection is Empty does “convertsTo” come into play.

Yet another future post will show how the type hierarchy gives Wombat named parameters with default values.

[update 2016-09-28: That last promise was never fulfilled. It's too easy for a post. If you want named arguments to a procedure, use a Struct parameter. Structs allow default values which have this effect: a Struct without the defaulted field will convertTo any type with extra fields that have defaults. Voila.]

Whither Wombat?

We interrupt the sequence of posts on aspects of Wombat for a couple of planning posts. This one on language design “decisions”.

1. Under the influence of Bob Harper, and also guys from the Mercury team, I am giving up my flirtation with lazy evaluation. It has always been my expectation that Wombat’s good support for closures would cover this. I now realise that I also need to handle memoization well. Anyway a fair bit of thought needs to go into making memoized streams as convenient as lazy lists, and also covering other lazy data structures.
2. Also from reading Harper, I see that he has had the same issue as me with the overloaded use of the word “variable”. My solutions was to use “mutable”. However he has already invented the word “assignable”, and since we don’t need 2 words for the same thing, I will, at some point, change the doc from “Mutable” to “Assignable”.

More substantively is the issue of the status of laws/axioms. It used to be that these were just comments. Then languages started including them in an executable form, with a bit of handwaving “quickcheck style checking programs might use this”. That’s where Wombat came in, and the way it is specified in the doc.

But I don’t think this phase will last long. It is time to do it properly and prove all claimed properties:

• Primitive types will come with axioms describing their behaviour, from the X86/JVM/whatever manual.
• The semantics of other Types will be proved from the code implementing the semantics using the assumed (if primitive) or proved (if not) semantics of the implementation.
• Other things that need to be proved include:
• proving that a supplied specialization does indeed implement the same algorithm as the original;
• proving that the procedures linking one implementation to/from a more comprehensive one (usual the main one) are inverses (where the reverse is defined).
• …

Just as the time has come for programming to help mathematicians deal with complexity, so it is time for mathematics to help control the complexity of programming. While this looks really ambitious, the main plan is to get the syntax right so that it can be brought in later. It is expected that initially the only proofs will be “admitted” (as they say in Coq). However it is expected to be extremely useful to think clearly about what should be proved.

A key decision needs to be made about WCTL: Wombat Compile Time Language. While the plan is for it to be a Wombat DSL, in the short term, to get going, it seems like a good idea to start with some existing scripting language which is well integrated with some target machine. A possibility is Pure which has a good interface to LLVM, and also to C code which could call more obscure parts of LLVM (like Integer overflow).

HoTT topics

HoTT stands for Homotopy Type Theory. Sounds scary and maybe it is. I’m slowly learning about it in various ways, mostly by watching Bob Harper’s lectures at CMU. The subject area of HoTT is “Proof Theory”. I’ve been known to say that Mathematics is about thinking clearly about problems. Proof Theory is mathematicians trying to think clearly about how to do Mathematics. While the details aren’t sorted out, there seems to be good reason to believe that HoTT is a major advance in this subject, and hence in Mathematics itself.

It has been known for many decades that there is a correspondence between logic and programming that is usually expressed as “Propositions are equivalent to Types, and proofs are the same as programs”. In HoTT this becomes true in a practical way. It looks like all or most of Mathematics can be formalized as files that can be checked by a proof assistant. Note that Mathematics is a human activity, and is about human understanding. So Mathematics can not normally be in a final form in these files since the implications for understanding need to be communicated in a human way.

In the world of Proof Theory we don’t have the law of the excluded middle. For a given proposition we might have a proof or a refutation, but until we do the status of the proposition is unknown. In Wombat there is a WeakBoolean type which also includes Unknown as well as True and False, and this has various applications which can be seen as being related to those in Proof Theory.

The core of HoTT is thinking clearly about equality. The very first bit about that (in Harper’s lectures 5 and 6) talks about the difference between Intentional equality, which follows by direct application of the definition of a Type, and Extentional equality which requires a more substantial proof. This has a close analogy in Wombat where primitive types are always Distinguishable (i.e. have a Boolean equality) just based on the representation as a string of bits. All types are then SemiDistinguishable (i.e. have a WeakBoolean equality) based, ultimately, on that Equality: I.e. (roughly) if 2 values of a Type are equal as bits then they are automatically equal, but finer concepts of equality (up to Distinguishable which excludes Unknown) require actual code (a “program” corresponding to a “proof”).

Wombat Types and their implementations

Wombat has quite a few little ideas in it, and one big idea. The big idea is this:

Types are defined by their semantics. A type can have multiple implementations with different performance characteristics.

Since changing implementation doesn’t change the semantics, the programmer doesn’t specify the implementation as part of the language. Programmers can influence the compiler’s implementation choices with pragmas.

An important addendum is that implementations need not cover all values in the type. There does have to be an implementation that covers all possibilities, and this is specified when the type is created. Here are some examples:

• Int is the type of integers.
• The comprehensive implementation is BigInt, which is, in turn, implemented by List Int64.
• The normal implementation is Int64.

If an Int64 operation overflows then the operation is rerun giving a BigInt result and the whole continuation of everything that follows is switched to one using the BigInt implementation for calculations depending on that value that overflowed.

• Array(Assignable X) is the type of traditional arrays from imperative languages: i.e. the bounds don’t change after creation but each entry can be updated. Wombat is functionally oriented, but not prescriptive. This example is the one that inspired the type/implementation split because the comprehensive implementation isn’t something one would normally want.
• The comprehensive implementation is just an array of addresses in memory where an X is stored. The addresses are not (necessarily) laid out in any neat way.
• The normal implementation is just a start address plus, in the 1d case, a length (and maybe a stride). Slightly more complex in higher dimensions.

This case is discussed in other blog posts: “Solving a 30 year puzzle” and “some history”.

• Any value known at compile time can be implemented by Unit. I.e. we don’t need to allocate any space on the stack to pass it as a parameter. Though it is a slightly complicated example, let us consider the expression s.length from the previous post. This is actually String.asProc(s).length, and in a normal way String.asProc(s) is just a closure returned from within the String.asProc code, and inside which s is locked down. In order for the compiler to use the zero length implementation of the Atom parameter, there has to be a specialization of that closure for when the parameter is exactly .length. Likely String.asProc is just one big case statement and this specialization will just throw away all the code except the little bit returning the length. So we see that for practical purposes we end up with the same result as in languages where a method does map to a special sort of procedure.

I won’t go on here, except to say that this is a very fruitful concept, and more examples will appear.

I gave a talk on this once. The visiting expert at the end asked a question which I couldn’t understand, and hence answered incoherently. Afterwards I realised that he was suggesting that this was the same as interfaces/traits. Obviously my talk did not do a good job of explaining the concept. Or maybe the visiting expert was jet-lagged. Anyway this reminds me: if anyone wants me to give a Wombat talk, let me know and I’ll figure out if I can get there.

[update 2014-09-27: I should have mentioned the interconversion rules for implementations, which is a key thing that is different from interfaces/traits where no interconversion is expected. Every new implementation has to give a pair of functions for converting to/from some other implementation (commonly the initial universal implementation). The "to" direction has to be 1-1, and the "from" direction fails for values that aren't covered by the new implementation.]

atoms in Wombat

Since I'm too busy/weak to do more important things, I'm going to do some posts on specific aspects of the Wombat design. Hopefully this will be easier to understand than the doc "Outline of the Wombat Programming Language". I'll try to do it in an order that avoids too many forward references.

Lisp has always used atoms a lot, and perhaps gave them a bad name in the early days by adding a mutable value to each to give dynamically scoped mutable variables (yikes!). Wombat separates atoms firmly from variable identifiers by using a different syntax. An atom is an identifier preceded by a dot ("."). So .length is an atom. The only property of atoms is that they are distinguishable, so they can be easily used in conditional constructs like “if” and “case”.

The syntax is carefully chosen (i.e. it’s a hack) because the main use of atoms is to pick out methods. The expression s.length can occur in many languages. However in Wombat the dot is not a syntactic element, it is just a part of .length.

Of course lisp variants use atoms to pick methods as well. This looks like it is creating global names (as some uses of atoms in lisp do), but it isn’t. In any language where we can write s.length, the “length” method clearly has its meaning restricted to the context of s. In effect s is acting as a namespace of names that are relevant to it. This is much nicer than python’s len(s), in which len is a name polluting the global namespace, but without a clear meaning independent of s.

Well I had to laugh. Of course Haskell field selectors avoid the imaginary abuse of global names. But I notice that the next version will have a feature: OverloadedRecordFields. Yes, Haskell has rediscovered atoms.

In Wombat the expression s.length is a function invocation. It just follows the Haskell style in which the function is immediately followed by the parameter, and binds tightly to it. Parentheses are not needed when the parameter is a simple expression such as an identifier or an atom.

But, I hear you say, s is a String (let’s say) not a procedure. Yes, but in Wombat every value can act as a procedure. Every type, such as String, has a method .asProc which defines the behaviour as a procedure. So in this case, s.length means String.asProc(s).length. We gloss over the recursive character of this definition...

Atoms turn out to have other uses, but they are all similar in taking their meaning from a nearby context.