Multitype has gone!

Version 0.0.3 of the outline doc (https://docs.google.com/document/d/1sNnCvYFjjBmtrl7XF7JX_pdMZ_0ydrctjTR0pO0p5Y4/edit?usp=sharing) has been updated to remove Multitype and replace it with Empty weirdness, based on the fact that Empty is at the bottom of the isA hierarchy, so Empty isA X for any X.

• [] is a List Empty, so can be used where any List X is required;
• Option.none is an Option Empty, so can be used where any Option X is required.
• An explicit closure, { ... }, has type Any=>Empty, and so isA X=>Y for any X, Y.

We've drifted a bit towards dynamic typing, but all is now very straightforward.

Mathematics influences Wombat again

In Wombat, types form a lattice (an order lattice) generated by isA declarations. The sup/lub/join is Union, the inf/glb/meet is Intersection. Unions between otherwise unrelated types are new types created as required. The intersection is just the union of types below all the types being intersected. So, for some examples: Integer isA Rational, Integer isA GaussianInteger. Union[Integer Rational] is Rational, but Union[Integer String] is a new type (with few properties, just the ability to extract one or other). And, of course, Intersection[Rational GaussianInteger] is Integer. The intersection of unrelated types is the type Empty, which has no values.

[notational note: list entries are separated by spaces. The parameter of Union and of Intersection is a set of types, but can be given as a list as I have done here (because, in a forgetful way, List X convertsTo Set X). The / operator invoked below takes 2 Integers and returns a Rational.]

I've been following along, in a desultory way, with a Mathematics discussion (https://golem.ph.utexas.edu/category/2015/09/the_free_modular_lattice_on_3.html) where I learnt of the difference between a lattice (which has sups and infs for finite sets of members of the lattice) and a bounded lattice which also has sups and infs for an empty set of members. Things usually work better when you include these degenerate cases, so I thought: I wonder if I can make Wombat's type hierarchy into a bounded lattice.

It doesn't take much imagination to see that Union[] is going to be Empty. And then it is natural, looking at everything upside down, to see that Intersection[] is the type Any which is the Union of all types.

Now consider the list [7 3/2 4/5]. What is this a list of? It is naturally a list of the Union of the types of its elements. Since those types are Integer and Rational, the result is a List Rational (as any ordinary mortal would expect).

So what is the type of the empty list []? The set of types of the members is the empty set. The Union is thus type Empty. So [] is a List Empty. But we've seen that Empty is below any other type X, so Empty isA X. So a List Empty isA List X for any X. Which is exactly what you need to allow the empty list to be used in the situations where one might want to use it.

Syntax is a minor matter

I just learnt of the existence of Marpa: https://jeffreykegler.github.io/Marpa-web-site/. Basically this generates a BNF parser that is simple and efficient. I'm not sure how easily Wombat's user-defined syntax system can be implemented with Marpa, but the key point is this:

Having syntax built in to a language definition is going to alienate people. It isn't necessary. A core aim of Wombat is that different folk can use different syntax systems, including rolling their own, and still use each others libraries without difficulty. Of course Wombat will have default syntax for the standard libraries, based on the prejudices of the core developers, but even that can be easily changed. You prefer to separate your list elements with commas instead of spaces, or you like your "if" expressions to end with "fi": easy to do. Wombat may provide standard WCTL (Wombat Compile Time Language) functions to allow programmers to specify common styles.

What is important is the structure of the Type system. This is where I think Wombat is different (though the relevant literature is vast, so I could well be wrong). If a Rational has a denominator of 1 (or a Gaussian Integer has an imaginary part of 0), then it is an Integer, and not distinguishable from an Integer that arose in a more obviously Integer way. If two types have a non-Empty intersection (as Gaussian Integers and Rationals do) then you are not allowed to define a lossy conversion from one to the other: Conversion can only happen losslessly by going down to the intersection and then up (and it may then, naturally, fail).

I trained as a Mathematician, and I think this is the way most Mathematicians operate most of the time. Sometimes they will show a bit of guilt by writing "by abuse of notation", but I think they really feel it is ok. By contrast Mathematicians involved in the foundations of Mathematics don't allow this sort of thing at all. I suspect this is a big part of the disconnect between the two camps. Programming is in a funny state, being a mixture of very hacky stuff on one side, plus stuff that has come over from work on the Foundations of Mathematics. I think that Wombat, by contrast, has the right balance, corresponding to the way most people think.

On Infinite Things

Infinite things don't really exist. Consider the simplest example: the natural numbers 0,1,2,3,... We have strong intuitions about this set and we use that intuition in applying mathematics to the real world. Yet everything about Nat, the natural numbers, follows logically from the following simple, and finite, set of rules:

• Zero and Succ are primitive entities, completely defined by the following:
• Zero belongs to Nat;
• Succ maps from Nat to Nat. If N belongs to Nat, then Succ(N) belongs to Nat.

The recurrence relation is real but not easy to think about. The infinite set of natural numbers is something we are more comfortable with.

Consider the test program in the recently released first draft of Wombat compiler code:

   `fact1 _n = if (_n:Int>=?0)==0 then {1} else {_n*fact1(_n-1)};

   `fact2 = { `n = $:Int>=?0; if n==0 then {1} else {n*fact2(n-1)}};

   `in = getInt();

   putInt( fact1 in = fact2 in)

To understand the first line, consider this very finite situation. We have 2 expressions within a closure:

1. `not true = false
2. `not false = true

The first thing to note is that it is OK to declare the same name more than once in a closure as long as the names are compatible. Being equal is the simplest form of compatibility. The other acceptable form of compatibility is by combining procedures, and that is what applies here. For the gory details see http://wombatlang.blogspot.com.au/2015/05/combining-procedures-in-wombat.html. But basically they have to agree (or be combined!) where they overlap, and where one fails (harmlessly = Fail.next) and the other doesn't, the combination takes that value. The declared name can't be used until all declarations are complete.

Getting back to that first line above:

   `fact1 _n = if (_n:Int>=?0)==0 then {1} else {_n*fact1(_n-1)}

The first thing to notice is that this expression is the left parameter of a semicolon(;) operator, so the value is discarded, and only the side affect (defining fact1) is relevant. For the record the value would be a Type.

The expression involves a free variable (_n). That means this is an application of a Wombat macro. Since no macro is specified, the default applies, which is "forall". So this is really:

   forall _n (`fact1 _n = if (_n:Int>=?0)==0 then {1} else {_n*fact1(_n-1)})

This is the same as our definition of "not" above, except that there are an infinite number of procedures to be combined (all possibilities for which the expression doesn't fail):

   `fact1 0 = if (0:Int>=?0)==0 then {1} else {0*fact1(0-1)}

   `fact1 1 = if (1:Int>=?0)==0 then {1} else {1*fact1(1-1)}

   `fact1 2 = if (2:Int>=?0)==0 then {1} else {2*fact1(2-1)}

   ...

Except that it is not to be regarded as being in any order.

Note that we can refer to fact1 inside the definition because that is inside a closure. It is technically a forward reference which is filled in, completing the construction of the closure, when the definition completes. The closure can not be called until all forward references are filled in.

[update 2016-09-28: This is no longer quite correct in the new wombat.]

Wombat changes

Here are some changes to Wombat:

1. The type that was Void is now Unit. Its only value, that was empty, is now unit. This is cutting a link to Algol68 usage, but the new naming is a modern standard.
2. I plan to allow operators to have prefix and left-parameter forms. This will allow the "-" in 5-3 to be different from the "-" in -3. What happens to the right can then be different for each. So prefix "-" can have a higher right priority to infix "-". This will also allow the Python3 "if" style. It will allow the whole APL/J monadic/dyadic suite for those that like that sort of thing. [Previously Wombat could handle -3 because it became unit-3 which could be handled differently via polymorphism.]
3. The type Muteable X [which used to be Var X before that] becomes Assignable X, following the lead of Robert Harper.
4. Wombat will make more use of 1-tuples. The 0-tuple type is exactly Unit. The comma operator generates n-tuples for n>1. There is no syntax for 1-tuples, just procedures to go to and fro. Previously I vaguely thought that X and Tuple[X] were the same, which caused various problems. Now all is sweetness and light, and I can, for example say that Option X is just Union[Unit,Tuple[X]], and even if X=Unit, that still works because unit!=to1tuple(unit).
5. In addition to operators for tight and loose breaks, add breaks representing line breaks with various sorts of indentation change.

[update 2016-09-28: point 4 is rubbish.]

Super Simple Syntax

Super Simple Syntax

“Perfection is achieved, not when there is nothing more to add, but when there is nothing left to take away.” ― Antoine de Saint-Exupéry

Wombat likes to take minimalism to extremes. The only built in types are procedure types and tuples (Which includes Unit, the 0-tuple). There is no builtin syntax. All syntax is defined with the syntax creation scheme called Super Simple Syntax (SSS) which is available to library writers and even end-users. If the programmer doesn’t like the syntax she can make big or small changes, without affecting interoperability with other modules.

Some programming languages have user defined operators with just one precedence number that is the same on both sides. This means that you also have to specify left or right associativity. In Wombat the left and right can have different precedence. The operator associates to the left if the right precedence is higher.

Wombat allows operators with no left operand, or no right operand, or both. Indeed an identifier is just an operator, with no left or right, from a syntactic viewpoint. Operators can have following sub-operators, such as then and else for the if operator. Sub-operators can repeat or be optional, and can have a nested structure. There can be repeating groups, such as elif-then pairs in an if operator.

Operators can have a left parameter in which case they have a left priority. They can have a right parameter in which case they have a right priority. Technically the right priority belongs to trailing sub-operators such as else, but this is commonly the operator itself when it doesn’t have other sub-operators. (The operator counts as a sub-operator of itself.)

An operator can have a sub-operator (not itself) which is also in use as an operator. It only takes its sub-operator meaning where it is expected.

Priorities form a partial order. If priorities are not comparable then they can’t do battle for an expression between them. This stops different libraries from getting in each other’s way. The partial order includes as a subset the positive decimal numbers with a finite number of digits (Dewey decimal style), which the ordinary programmer might prefer to use. Additional priorities are defined by names together with enough comparisons between each other and (if desired) the numerical priorities. The partial order is the resulting transitive closure.

Most operators just map to a procedure. The parameters are combined into a tuple in the same order that they occur. Repeated parameters map to an n-tuple where n is the number of repeats. Optional parameters map to a 0-tuple or a 1-tuple. The procedure has to be appropriately polymorphic.

Every (sub)expression starts with an operator with no left and ends with an operator with no right. Every operator with no left is the start of one or more expressions, and every operator with no right is the end of one or more expressions. Every operator with no left will be preceded by a suboperator with a right which will swallow one of the expressions it starts. Every operator with no right is followed by an operator with a left to swallow one of the expressions it ends.

When an expression is required after a (sub)operator, and the following operator has no left, then the 0-tuple (unit:Unit) is inserted automatically. This means that unit can be written (), but also that it can be omitted almost anywhere that it might appear. [Note that '(' is an operator in Wombat, with ')' as a suboperator.]

When an operator with no right (such as an identifier or a parenthesized expression) is followed by an operator with no left, then a space-break token is inserted. In standard Wombat this is left associative procedure call. Actually if there is no actual white space (the break is created by the lexical analysis) then it is a different operator: tight-break. This also maps to procedure call. Tight-break is always an operator: it can't be used as a suboperator. Space-break can be used as a suboperator, and is so used in the list constructor operator (e.g. [12 34 56]).

Some initial code for SSS has been released. See the preceding post and https://github.com/rks987/wombatlang.

Very early code available

Some new languages have come out with a facility for user defined syntax that is quite weak compared to Wombat's. So I thought I'd code up (most of) Wombat's Super Simple Syntax. It is available at https://github.com/rks987/wombatlang. Pull requests welcome! It's not too late to become a founding father/mother of the Wombat Programming Language.

A blog post on Super Simple Syntax will follow this.

The code released is just enough to generate the AST for one small program. it is written in a simple recursive descent style using Python 3.4. Sadly it is not in Functional style. I have no idea how to do that for this program. Advice welcome (pull requests more so).

The SSS code does cover more than is required for the example program, so there is untested code. On the other hand there are features, such as sub-sub-operators and repeat groups, that are not yet implemented.

One reason the code is in Python is because it is the probable choice for the language for an initial version of Wombat Compile Time Language (WCTL). However maybe we can define WCTL as a JSON network API, so WCTL libraries can be written in any JSON-compatible language.

This is my first go with git and github. Let me know what I should be doing.

Blog post on hacking Scala

https://meta.plasm.us/posts/2015/07/11/roll-your-own-scala/ is a fun post on making Scala do things it doesn't want to. The problems solved are not supposed to be problems in Wombat. However they are likely to be a problem in the implementation of the compile-time parts of the language. So it is interesting to think about the sort of simple constructs that can be cajoled, in code most users never see, to do the right thing.

Wombat and Mathematics

I was disappointed at the somewhat downbeat tone of Mike Shulman in https://golem.ph.utexas.edu/category/2015/06/whats_so_hott_about_formalizat.html#c049290. I had thought HoTT/UF was going to solve all our problems.

Trying to follow along with some of these discussions I see things that seem similar to issues that I try to address in the design of the Wombat programming language.

In the discussion of the merit of type theory versus set theory we see a comment suggesting that in the set theory world we have to worry about whether 1∈2. That’s because the natural numbers are modelled in set theory as: 0 by ∅ (empty set); 1 by {∅} (the set with only the empty set as a member), 2 by {∅,{∅}}, and so on. Yes the natural numbers and their properties can be modelled in set theory this way, but the properties of natural numbers are different from the properties of these sets. This is similar to the way Wombat types are built up in steps from primitive types. A type and its properties are implemented using some other type and that type’s properties, but there is no automatic carryover of properties. This is in contrast to the longstanding tradition in programming languages of identifying types with their implementations. It seems from the comment that mathematics has the same problem.

Another current issue in Mathematics is the meaning of equality. A comprehensive discussion with links is given in http://ncatlab.org/nlab/show/principle+of+equivalence, but also look at John Baez’s first cut of that page http://ncatlab.org/nlab/revision/principle+of+equivalence/1. Wombat allows each type to have its own idea of equality (not necessarily with excluded middle). The problem, very similar to the mathematical one, is to ensure that if x=y then f(x)=f(y) for any function f. For example one of the permitted implementations of rational numbers is as two integers in unreduced form. We need to ensure that functions don’t peek at the representation and return a different result for 6/4 compared to 3/2. In Wombat a Type has properties and axioms. For each implementation of that type the properties are implemented in terms of the underlying type, and the axioms are proved using the axioms of the underlying type. Also when there are multiple implementations, then the later implementations have to proveably give equivalent results to the initial (reference) implementation. Other functions can only access a value through the properties of its Type, and this prevents them from doing the evil thing and peeking at the implementation.

A related question is whether two things can be equal if they are not the same type. Wombat handles this by having a hierarchy (order lattice) of Types. Every value belongs to a hierarchy of types, and values can be compared anywhere in the intersection of the two hierarchies. If the intersection includes the Empty type then they aren’t equal, though this isn’t the way the issue would normally be decided.

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