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.

expanding the derivative

The arithmetic derivative (discussed here: https://plus.google.com/101584889282878921052/posts/9nY35Ma1pbU) is cute but perhaps not that important.

However differentiable functors seem important for programming. They take data structures and return a "one hole context" for that structure. This makes it possible to write code that traverses data structures in a very general way.
In http://stackoverflow.com/questions/25554062/zipper-comonads-generically/25572148#25572148, Connor McBride shows how this can involve partial differentiation. Wow.

As we see it is pretty messy in Haskell, even with multifarious optional features enabled. I suspect that this is stuff which is an indicator of whether you've got your programming language design right.

Yin Wang talk in 2012

It would have been nice to hear Yin Wang's talk in 2012 (from http://lambda.soic.indiana.edu/talks-fall2012). Sadly some of his posts have disappeared from his blog. I wish I'd kept a copy.

Oct 19: A Fresh View at Type Inference

Speaker: Yin Wang

In this talk, I present a simple and unified understanding of type inference systems ranging from the simplest to the most complicated. Those include:

• The polymorphic Hindley-Milner system
• MLF and its contemporaries
• Intersection type systems
• Polar type systems and bidirectional type checking

I attempt to answer the following questions:

• What are the key intuitions behind type inference?
• What is wrong with let-polymorphism and how to fix it?
• Why are type systems more powerful than Hindley-Milner system seldom used?
• Why is there always a conflict between expressiveness and effectiveness and how to find a balance point?

This talk is suitable for both beginners and advanced researchers. No prior knowledge of type systems and typing rules are required. Some understanding of lambda calculus may be helpful.

Simula67 and the threaded stack

Simula 67 is just a few years from its 50th birthday. It was a long way ahead of its time. One of the things that made it possible to do all the things it did, like simulated or real time concurrency, was that it didn't use the hardware's simple but efficient stack. Instead it threaded the stack on the heap. This made it easy to have multiple stacks going simultaneously. [However it was stupid that, at least when I used it, it didn't return popped memory to free, but just left it around for the garbage collector.]

This seems like it would naturally make it a lot easier to have programs containing laziness, concurrency and parallelism, with separate processors working on separate subexpressions. Forty years ago the extra overhead of threading the stack was too inefficient (and we were pleased when C came along, even though it was much less powerful). But now I think it would be ok. Even better if memory technology supported it.

[update 7-Sep-2014: My old brain finally remembered that in Simula67 an object was just a function that left its local variables and inner procedures lying around after it finished. Also you could transfer pointers (refs) to local stuff without problems because these stack areas wouldn't be GCed if there were pointers into them. So there were substantive reasons why it worked as it did.]