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.]

lazy closure creation

Some issues with closure creation become more important in a lazy environment. Consider this simple Wombat Void=>Int closure:

{ x+y }

Since the add doesn't involve the (empty) parameter, it is a subexpression of closure creation, not of closure execution. In an eager environment we mightn't want to do the add until the closure is called to avoid doing it unnecessarily (this would be more clear if it was a more expensive operation). But (yet another) nice thing about being lazy is that we can do these things correctly without cost (apart from the cost of laziness itself).

It is not so easy to switch Wombat to being lazy. The intention was that the language would have 3 levels:

• A very low level that maps directly to the particular hardware format. Let me call this a grade in Mercury style. This is the primitive procedures and types that vary with grade.
• The next level up is C-like and abstracts out the grade-specific crud, but still doesn't provide a safe programming environment for most uses.
• At the top level we have types and operations with mathematically nice semantics, designed for most uses. This is where laziness might be appropriate.

parallel laziness

I've just started reading Paul Bone's thesis: https://mercurylang.org/documentation/papers/pbone_phd_thesis.pdf. I got to the bit that said "laziness makes parallelization harder". That set me thinking. Here is some idle speculation.

When we are executing our lazy program we can look at every possible expression in our program, and classify them:

• There are expressions that we need to evaluate to advance the next IO. This includes all subexpressions that we will definitely need to evaluate.
• These have subexpressions that we might or might not need to evaluate. In wombat these will always be in closures. Note that creating those closures (filling in the values of identifiers) is also an expression.
• On the other side of the coin, and working from the bottom up instead of top down, there are expressions that we could evaluate because we have all the parameters.
• And conceivably we could order these by how likely the value is to be useful, either for the current IO or for possible future IOs. And conceivably we could improve this ordering as time goes on, based on the actual behaviour of the program.

So one can imagine a program that has as many cores as the operating system wants to give it at any particular time. And those cores can beaver away on all the available work that can be done...

And doesn't this remind me of work that was going on in the next lab when I was younger: http://www.eganfamily.id.au/archive30nov2007/monash/research/projects/CCC/index.html. (Actually their lab was up the road at RMIT since it was a joint CSIRO-RMIT project.)
[update!! And I got this wrong: the Prof Greg Egan is not the the Greg Egan (http://gregegan.customer.netspace.net.au/) who is an author and amateur (I presume) mathematician who collaborates with John Baez]. I also see Mark Rawling in the photo. Later we (mostly Mark) wrote a C++ library for reactive programming that is somewhat related to this post. And I now remember that I applied for a job with that CSIRAC2 project, because of my interest in functional programming which they were using. I didn't get it :-(.

laziness, backtracking and explicit io threading

When I first heard about laziness in programming languages I thought "That's just an optimization technique". Then I saw the example of an infinite lazy list and I thought "That's just a stream, umm I mean a memoized stream [1]". Well yes, but streams are uglier and harder to think about than lists, and this quickly gets worse for more complex structures. So I've come around to being rather sympathetic to laziness by default.

And laziness seems closely related to an important emerging trend in programming, which is to allow the programmer, as much as possible, to write the program as specifications and tests rather than in the traditional style of "step by step instructions to a complete idiot". This is also related to the trend that the programmer gets to deal with entities with mathematically nice semantics rather than entities with hardware-level semantics (and this is an important aim of Wombat).

If we're lazy then we need something to inspire us to do anything at all, and in programming it is the need to do IO that provides the inspiration. And, of course, we need to do the IO in the correct order, so you come around to the need to explicitly tell the compiler when IO is needed and in what order. In Haskell that is done with the IO monad. I won't explain the details since Mercury has a similar but conceptually simpler system.

I vaguely knew that the Mercury programming language (mercurylang.org) also had explicit threading of IO. So when I learnt about laziness, I naturally assumed that Mercury was also lazy and that was the reason for the IO threading. Now that I have (finally) started to learn Mercury [2] I see that this is wrong. Mercury is a logic programming language, in the tradition of Prolog, but much more hard core about being declarative. The reason it is explicit about IO is because it supports backtracking when searching for a logical result. So it needs to thread IO to prevent backtracking into an IO operation that has already happened.

The way Mercury does this is that procedures which want to do IO (starting necessarily with main) have:

• an extra input parameter representing the world before the procedure is called. This parameter is marked "will be destroyed" so that it can't be reused after the procedure is called.
• an extra output parameter representing the world after the procedure returns. This value is marked "unique", meaning that there are no other copies of it. And naturally this has to be used as the input parameter of the next IO operation.

This could get tedious, but there is syntactic sugar to handle the bookkeeping. An obvious question is: Why does Mercury have eager evaluation instead of lazy, since it is declarative? Is there some interaction with logic programming and backtracking that makes laziness difficult? I don't know the answer to that, but here's a different question. 

How do you handle the important need for IO concurrency? In Haskell the guys from Facebook have recently released their Haskell library for concurrently reading from multiple sources. However they are careful to only claim to handle reading. So I'm guessing that handling concurrent changes to the world is not so easy.

In Mercury one can write code (I hesitate to say "function") where spawned procedures can fan out and rejoin (actually I don't yet know how to rejoin before end of program, but I'm sure it is possible). Anyway this is all nicely explained by Mark Brown in this email: http://www.mercurylang.org/list-archives/users/2014-August/007757.html. You need to learn some Mercury to understand it, but I recommend that.

----------------------------------------------------------------
[1] A stream is just a procedure (taking no input) which either returns an end-of-stream marker or it returns a pair consisting of the current value (like the head of a list) and the next procedure to call (like the tail of the list). By a memoized stream I mean that all those procedures are memoized (which means those procedures quickly return their result rather than recalculating it when called more than once).

[2] Learning Mercury is easier than on my previous attempt (15 years ago) because of the rather nice, though unfinished, tutorial by Ralph Beckett which is at the top of their documentation page.

-----------------------------------------------------------------
Update 2014-09-20: I just saw Bob Harper's post "The Point of Laziness". He basically endorses memoized Streams as doing the job of lazy lists. I'm inclined to be convinced, and Wombat's neat terse procedure format should suit. It is a challenge to handle more complex lazy structures nicely with procedures.

Update 2016-09-28: The current spec calls for values to start as holes and be passed around like that till set. This does some of the job of laziness. Streams can be created in interator/yield style, making streams much easier to use.

IO in a declarative or functional language

Haskell is declarative and functional. Its supporters seem to hang out more with the functional crowd. Maybe they think it is easier to sell "declarative" to functional folk, than to sell "functional" to other declarative folk. And there are good reasons why that might be so.

Suppose we declare that

y = x + 1

[This is not an assignment. Imagine a val in front if that is fits your language preferences]. This declares a relationship between x and y, but it does it in a functional style. It would look more functional still if we wrote "y = add 1 x", but that is just sugar.

But what if we have y and we want x? Since we are just declaring a relationship it isn't obvious why we have to change this. But in functional style this has to be changed to:

x = y - 1

Functional programs can only run forward, they can't run backwards. Haskell has, of course, a big exception to that: Constructors can be run forward (to construct) or backward (to deconstruct). But perhaps everything that can run backwards should be allowed to (and hence be useable in case statements). In addition to convenience there is a dodgy philosophical point.

When we look at the way the world works it is rather like a giant computer program. And it is particularly like a program in that, on a large scale it pushes forward in an irreversible way. Entropy increases and broken plates never reassemble themselves. And yet at the core is quantum mechanics which is completely reversible.

Haskell and Mercury are two languages in which the interaction with the external world (including mutable data in memory) is explicit. This is a consequence of the fact that both languages are declarative. In non-declarative languages the textual order of the program specifies an order of execution (optimisers alter that, but they are constrained to preserve the semantics, and are forced to make conservative decisions as a result). In declarative languages the compiler generates execution when required, and the thing that brings about that requirement is interaction with the outside world. Since that interaction is explicit, one would hope that the optimiser is never constrained by worrying about what separately compiled code might do.

So it seems that programming should have three levels.

• A core language that is reversible. This specifies what can be handled by cases, though if you allow multiple returns (as Mercury does) then you can expand that.
• Reducing operations (like summing a list) which are intrinsically irreversible.
• Interaction with the unforgiving world which forces an order of execution.

But maybe its not quite that simple. It seems that if the part of the real world you are dealing with is quantum then it might be reversible and you might conceivably be able to interact with that in the reversible part of the language. Perhaps more practically: When two programs interact with each other then they might sometimes be able to do that while each stays within the reversible core.

I should have another go at learning Mercury. Last time was 15 years ago.

infinitesimals for programming

Per Martin-Löf has played a major role in uniting our ideas about mathematics and programming. So I was impressed to see this quote from 32 years ago:

I do not think that the search for logically ever more satisfactory high level programming languages can stop short of anything but a language in which (constructive) mathematics can be adequately expressed.Per Martin-Löf. “Constructive mathematics and computer programming” (Logic, Methodology and Philosophy of Science, 1982)

But things are getting HoTTer, and now it is possible to glimpse a world where all mathematics can be regarded as constructive. Or, at least, amenable to integration with programming.

Some real numbers, such as 3.7 and π, are computable in the sense that you can write a program to get as many decimal places as you want. Computable numbers are part of constructive mathematics in a clear way. But most of the reals aren't computable. In some sense those non-computable reals don't exist. But clearly our understanding of the reals helps us think about the real line, and many other important concepts. And the way the reals are constructed and reasoned about creates a consistent mathematical context. And that combination of usefulness for human thought and logical consistency defines the boundaries of mathematics.

Infinitesimals seem even further from constructive mathematics than non-computable reals, but actually that is not true. They are certainly useful for thought and they can be used consistently (as I remember from Uni in the early 70s). So imagine adding infinitesimals to the numeric types. I'll leave the programming language details rather vague. It isn't Wombat, though it could easily be changed to be:

def differentiate T::RealLike==> (f:T=>T) T=>Option(T):
    def dfdx(x:T) Option(T):
        val dx = Infinitesimal.new
        return Infinitesimal.to[T]((f(x+dx)-f(x))/dx)
    return dfdx

We presume that arithmetic operations on our float+infinitesimal are just the symbolic calculation we would do. Sometimes (depending somewhat on the cleverness of our libraries) we will end up with a numerator that can be divided by dx, leaving something which the to[T] function will handle by eliminating the Infinitesimals in a safe way. This works easily for polynomial functions as we remember from school. When it doesn't work we return Option.none.

We can call f with parameter (x+dx) because a RealLike type with added Infinitesimals is also a (different) RealLike type.

 

 

mathematics and programming

I wrote in my main blog about the collision between Mathematics and Programming: http://grampsgrumps.blogspot.com.au/2014/05/mathematics-and-programming-collide.html. More recently my corner of the twitterverse has gone mad on the subject of whether programming is mathematics.

Also recently, John Baez made a relevant comment on google+ (in a thread about learning R: https://plus.google.com/117663015413546257905/posts/T7foMTXinGG). Since we can't link to google+ comments, here it is:

I find that writing math papers, teaching, and explaining things online makes me as clear as I want to be.  Programming goes further, into making me clearer than I want to be.  I don't really want to explain something to a complete idiot who goes berserk and throws a temper tantrum whenever I make a simple typo.  :-)

 But Voevodsky would say that Mathematics has got too hard, and we need to explain it to a computerized idiot to avoid significant mistakes: http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2014_IAS.pdf.

The problem with serious software development isn't typos, it is the huge amount of stuff you have to know to get it done. Jonathan Edwards wrote recently (http://alarmingdevelopment.org/?p=865):

The way things are today if you want to be a programmer you had best be someone like me on the autism spectrum who has spent their entire life mastering vast realms of arcane knowledge — and enjoys it. Normal humans are effectively excluded from developing software.

Only a small part of that arcane knowledge is really the programming language. Most of it is in the libraries the programmer needs to use. In most cases the libraries give access to some aspect of the runtime environment. For example you can't use Google's App Engine libraries without a good understanding of the environment they operate in. And sadly it is often hard to use the bits that you want to use without understanding aspects of the environment that are not directly relevant but influence the structure of the library and the meaning of parameters.

It is mostly the availability of libraries that determine what language we choose to work in. For App Engine one is almost constrained to work in Python or Java, maybe Scala or Go. Clojure runs in the Java environment (JVM) and has a clojure style library for App Engine, but that library isn't kept very current. One could conceivably use Haskell by using the Haskell-to-Javascript compiler and running the javascript on the JVM using Rhino. Even if this worked (unlikely) one would find that there is no idiomatic Haskell way to access App Engine and one would have to write lots of horrible syntax to access the Java libraries from javascript, and use the mechanism for calling javascript routines from Haskell. Similarly we see that people doing statistics use R, because it has the libraries and builtin functionality required.

Increasingly everyone in the world will need to do bits of programming at times. That's why we have spreadsheets and statistical packages. R is more than that, but many would say it is too flexible and idiosyncratic for developing large programs safely. We have, in recent memory, seen an Economics paper that was very widely reported, that was subsequently shot down because it had a bug in an Excel spreadsheet.

What we need is for computers to understand a lot more about what we are trying to do, so they can help us more. On the one hand this means that programs should look more like specifications and tests. And researchers are working on this. The other thing is that programming environments just need to have good general knowledge.

And, as it happens, Stephen Wolfram is working on this. For example here is a list of file formats that the new (Mathematica-based) language supports in various ways: http://reference.wolfram.com/language/guide/ListingOfAllFormats.html. [It doesn't seem too much to ask that an interactive environment be able to guess the format of a file and offer you code to access it.]

Mathematics is about thinking clearly, so we expect that good support for it will be the most important thing in facilitating correct programming. The Wolfram Language knows a lot about Mathematics, as we expect from its Mathematica background, but I don't think it is in the best form to be useful. Maybe I just don't understand it yet.

Yin Wang on mutable and immutable arrays

Wombat can easily accommodate Yin Wang's ideas on arrays: Design mistakes in Swift language’s array.

In Wombat a 1-dimensional Array is immutable and the same as a List (see footnote). To get a mutable Array of X you instead create an Array(Assignable(X)). Conceptually it is a fixed array of addresses in memory. And we can easily create an operator similar to the proposed [[1,2]]. It would create an Array(Assignable(Int)) with 2 entries initialized to 1 and 2 respectively. However the specific syntax is taken (being a one element Array whose element is [1,2]). But something similar like ≪1,2≫ is ok.

footnote: Traditionally a List was a singly linked list where you could efficiently prepend values, and an array was a contiguous block of memory. However the semantics can be identical (with differing efficiencies). Languages should be about semantics and not about implementation and efficiency. The programmer should mostly leave efficiency to the compiler, with the occasional pragma.

[update: just changed Mutable to Assignable]

overlays, shared libraries, and all that

Once upon a time you would link your program with everything it needed, and after that it stayed the same (unless the operating system calls changed behaviour).

But memory was insanely expensive so programs soon didn't fit. I well remember trying to get overlays to work.

So we invented virtual memory and shared libraries. Shared libraries had other advantages. Without changing your program you could get performance and security upgrades to the libraries which improved all the programs using that library. Sometimes there were also functionality improvements and we see that a lot in the smartphone/tablet world with google moving a lot of functionality out of the operating system and into a library.

So we've got stuck on shared libraries even though they bring up a big problem for the developer: version hell. This is where one library requires specific versions of another library. Then you want to use a different library as well, and it requires a different version of that 3rd library.

Memory is now cheap, so really it shouldn't be beyond the wit of man to design a system that incorporates the advantages of shared libraries without the problems. Or maybe allow old fashioned linking, but still allow updating without relinking main. At any rate it is obvious that different libraries should be able to grab stuff from other libraries without getting in each others way. It doesn't matter if there are multiple versions of the same subroutine in memory. It should be said that libraries should never use global memory: if they want global memory they should map a file with the particular level of granularity they want.

This post was inspired by this observation from the new Swift blog:

"Xcode embeds a small Swift runtime library within your app's bundle"

But this seems to be a temporary thing, not an attack on the problem.

Invariants

I well remember watching this talk from Google I/O 2009: A Design for a Distributed Transaction Layer for Google App Engine. The general message:

Programmers should concentrate on invariants in the software.

And it was interesting to see them apply this is in a very specific case (where I happened to understand the problem and the context).

And I wondered whether programming languages and libraries could support this approach better.

This paper and talk by Bob Atkey looks like it is very relevant: From Parametricity to Conservation Laws, via Noether's Theorem (slides). Unfortunately understanding it is a bit of a way down my stack.

negative and fractional types

I'm entranced by http://www.cs.indiana.edu/~sabry/papers/rational.pdf: "The Two Dualities of Computation: Negative and Fractional Types" by James and Sabry from Indiana Uni. Amazing. Not that I really understand the implications.

Note that it is about a reversible language which can't be a full Turing complete language. But the reversible parts of a language are very important. They arose naturally in the design of Wombat where inverse pairs are important in a number of places. An explicit procedure takes the input and generates an output by unification. A single explicit procedure can generate an inverse/adjoint pair of procedures if the input ($) and output (`$) can be interchanged and produce a valid inverse procedure.

So I would love to understand the paper better and build it into Wombat, making the reversible part of the language a more important core part. Mercury is a language which puts special emphasis on the reversible bits. I should learn more about it.

There is a fascinating similarity to quantum mechanics, which is a core and reversible part of physics. And of course, the next level up in physics, where time only goes forward and entropy increases, then seems to have some similarity to a complete programming language. Hmm...

Swift and Mercury

Some of the things in Swift look a bit like wombat. Types acting as namespaces, at least for enumerations. Also we see "." as a prefix which gives the appearance of wombat atoms. Of course Swift is much more ad hoc than wombat.

It is nice to see the Mercury language getting more activity. It was an inspiration for the invertible functions in wombat, and I am sure there is more improvement to be made in that aspect of wombat.

Yin Wang on type inference

[update: Note that Yin Wang has deleted his post. Maybe he no longer agrees with it.]

Wombat hasn't made much progress recently. However I was delighted to discover Yin Wang. Basically his talk on type inference, http://yinwang0.wordpress.com/2012/10/19/type-inference/, explains why dynamic typing works where static typing seems to often get in the way.

He also says elsewhere that static typing is not much different to, nor much better than, static analysis of a dynamically typed language. This is very hopeful for Wombat, because Wombat's planned static typing is just based on static analysis, which is a required part of the language, not an add on.

some history

When I started there was really only assembly (machine) language. Assembler has some features that were right, but somehow the higher level language designers didn't like. In particular, every identifier stood for a constant value. For labels this was a memory address, but identifiers were also used to give names to constants.

The exceptional language design in which identifiers stood for constants was Algol68. Unfortunately it had some serious problems. If you used it you realised that it was hard to use, but the reason was not obvious at the time, but is with hindsight. The (main) problem was that it used Ref for variables and for pointers. That's just what we do in assembler, but it isn't confusing in assembler because there are no coercions. For variables you want Ref X to coerce to X, but for pointers you don't. Another problem was that Algol68 allowed procedure values, but since they weren't closures they were not very useful.

[In the previous paragraph I used the word "variable" to mean a mutable value, as opposed to a constant. Unfortunately the word is also used for other things, such as any identifier whose value is not known at compile time. That's why Wombat now has a type Mutable X instead of Var X [update: name changed to Assignable X as per Robert Harper]]

Serious programming that wasn't assembler became possible with BCPL (which later led to B and then C). It had procedure values and I remember trying to create a closure (not that I'd ever heard of the name). I remember saying to my boss "This should work but I don't think it will". It didn't.

Other languages were becoming available. In particular Simula 67 was a mile ahead of its time and I wrote some programs in good OO style before that style had a name. But I was more attracted to the ideas of functional programming, which were espoused seductively by W.H.Burge in the IBM Systems Journal: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?tp=&arnumber=5391254.

Once you have closures, and they can be full values, then you don't need any other mechanisms for control flow. For example if-then-else can be just a procedure with 3 parameters: a boolean and two closure parameters (each with no input and compatible output). I designed and implemented a baby language based on this idea and wrote it up for SIGPLAN. They managed to publish it even though I got the formatting all wrong: http://dl.acm.org/citation.cfm?id=988090.988097.

But my thinking ran into a brick wall. I wanted everything to be a procedure. In Algol68 an Array X is immutable and behaves just like a procedure. But how do you do a normal mutable array? Algol68's solution is to say that you can index a Ref Array X, and when you do you get a Ref X that you can assign to, allowing the array to be updated in place. This didn't seem right. A Ref Array X should point to an immutable array. What we really want semantically is an Array Ref X so that when you index it you naturally get an lvalue you can assign to. But that seemed like it meant a sequence of addresses which could point anywhere.

At this point I moved to CSIRO and spent 20+ years doing system management and research related to Internet security and commerce. But when I retired I started to think about it again, and I had an inspiration: Define types by their semantics and allow multiple implementations which need not cover all cases. This solved my problem because now an Array Ref X (Array (Assignable X) in Wombat speak) can have the expensive implementation of being a lot of possibly unrelated addresses, but it can also have the normal case implementation of a start address and length (and stride).

Semantic types had many other advantages, but there were still problems to solve. More on that another day.

the wombat has landed

[update 2016-09-28: The outline is up to v 0.0.4. Have modified this post to change Mutable to Assignable.]

I've been working on the Wombat programming language (under various names) for 35 years. I finally have a design that I'm happy with, though I expect that feedback from others (if I get any) will lead to useful, and even necessary, changes.

So I'm happy to release the document "Outline of the Wombat Programming Language". It is in Google Docs, with comments enabled. Comments can also be added to this blog post. In google+ see +WombatLang and/or use #wombatlang. An issue tracker is available at https://code.google.com/p/wombatlang/.

[update: I'm happy to give talks about wombat to any group (or anyone) who is interested, within financial contraints. Within 3.5 hours drive from Melbourne or Sydney should be ok.]

The doc starts:

Wombat aims for simplicity and generality in a comprehensive modern programming language:

• Expression language with simple left to right evaluation;
• All optional, repeated, deferred or parallel execution through a single mechanism: the anonymous procedure (closure).
• All identifiers stand for a constant value of some type. [Mutable variables are of a Assignable(X) type, whose constant value is effectively a memory address.] Identifiers in closures are set to their value at closure creation, and there is no confusion about what that means.
• Identifiers are just compile-time names with lexical scope. Identifier values are set by unification.
• Polymorphism resides in values, not identifiers or operators.
• Operators are defined in a simple way, available to users, which supports suboperators (like then in if-then-else). This covers nearly all syntax.
• Compile time entities and run time entities are handled with the same syntax. For example List is just a Type=>Type, and there is frequent use of tuples, lists and sets of Types.
• In mathematics, infinite entities are studied, whether formally (coq) or informally (latex), by finite strings from finite character sets. Wombat copies this, letting the programmer work conceptually with simple infinite entities at compile time.
• Operator macros utilize free variables to allow syntactic sugar, but also, more importantly, to provide a way of dealing conveniently with infinite entities at compile time.
• Non-primitive types are defined by semantics. They can have multiple implementations.
• Disambiguation of expressions uses information from the operands (input), and of the required result (output), equally.
• The standard library is written in Wombat Compile Time Language (WCTL) and uses capabilities available to all library writers.
  
  
• Wombat allows rich text, using bold, underlining, subscripts and an extended character set, but ASCII equivalents are available.