The new operator system

Syntax

The new operator syntax takes its lead from another language (Agda?), However that language's system is less comprehensive, so my solution is more messy.

Instead of a separate way of introducing operators, we just allow a special sort of identifier.

Wombat2 operators are identified by the sequence of mandatory suboperators (such as +, or if-then-else), plus identifying whether an operand is required or absent in each slot (after each, plus one to the left of the first suboperator). We also need the left and right precedence at the start and end, which are decimal numbers greater than 0.

To simplify matters I'm removing subsuboperators, and optional suboperators. Optional can be handled by just having multiple similar operators, though there is the danger of combinatorial explosion. These capabilities can be added to the scheme later if desirable. We do still need repeating suboperators.

Firstly we make the rule that a suboperator can't include any digits.

Now we construct our identifier as follows:

• We have an initial backquote (`). This means two backquotes on first use, but first-use backquotes are not required at top (file) level where operators are likely to be defined.
• We then have alternating numbers and suboperators, starting and ending with numbers.
• A zero in a number spot means that no operand is present there. A non-zero number means that there is an operand required there. 1 should be used on internal operand positions.
• The left and right numbers are precedence numbers. If a decimal dot is included it must have digits on both sides.
• A repeating subop is indicated by following it with \*. This is zero or more times, so if you want one or more times then include the first instance separately. Note that if a repeating subop is the last subop then both it and the last mandatory need right precedence numbers.
• \S is the whitespace suboperator and \J is the juxtaposition suboperator. \\ is a single \.

So we can just write:

• `5+5.1 = myAddProcedure # greater right precedence means left associative
• `0if1then1else3 = myIfProcedure

Of couse you aren't allowed to define new ones of these that are incompatible with an existing one, such as by having different precedence, or different repeating groups.

Translation

We prefer to associate operators with relevant Behaviours. Consider x+y. We convert x+y to Monoid.add(T).op(x,y). The question is how we work out the type T.

The answer is that we search downwards from the type of x and from the type of y, until we find a pair of types such that there is a type above both that conforms to Monoid.add.

Firstly we'll suppose that our types are: Integer, Rational and ComplexInteger (i.e. Gaussian Integer), with Integer below both of the others, and all conforming to Momoid.add. Suppose we try to add a Rational and a ComplexInteger. There is no type that is above both so we have to move down. There are two solutions: If we move Rational down to Integer then ComplexInteger is above (or equal to) both. If we move ComplexInteger down to Integer then Rational is above both. So we have two possible operations and either or both will work if one of x and y can coerce to an Integer (either because it is Rational with denominator 1, or ComplexInteger with imaginary part 0). So we combine the operations, giving a result that is a Union of Rational and ComplexInteger, and which fails if neither wants to be an Integer.

Now  suppose there is a type ComplexRational, that is above Rational and above ComplexInteger. Then we don't need to go down at all. So we use Monoid.add(ComplexRational).op. This coerces both x and y up to ComplexRational and the addition happens there and always succeeds.

The plan is to do sensible things that are close to the way run-time typing works in dynamically typed languages.

Postscript

Note that Monoid.add means the same as Monoid(.add). Since .add is an atom, this means Monoid is a Proc(Atom,Behaviour). This lets us distinguish different ways that a type can be a Monoid. Presumably there will be a Monoid.mul and a Monoid.max and others.

Typed TLA+

 As per the previous message, I think wombat2 is a good fit for TLA+, both at the pluscal level and the TLC/TLAPS level. 

So I think a more useful thing to do than my current effort will be to create a typed version of TLA+, using my type system. I think it is possible to create a full general purpose programming language that contains TLA+ (approximately) as a part.

I plan to match the syntax very closely, within the limitation that my syntax system can't do backtracking.

Don't hold your breath. I'm guessing it will take years. If anyone wants to help please leave a comment. Left to my own devices I will plan to use: my syntax system; python; copy the TLAPS method of talking to backend solvers (however when there is a proof I eventually want to bring it into the language as wombat2-style code). I'm open to alternative plans (that don't mention java).

Firstly I need to get into actually using TLA+ for a while.

TLA+ to Wombat2 correspondence

  I looked at TLA+ a decade or so ago and didn't grok it. I looked at the wrong sort of documentation. This time I looked at Lamport's "science" technical document: https://lamport.azurewebsites.net/tla/science.pdf. Surprisingly TLA+ has a lot of similarities to Wombat2. Here is the approximate correspondence.

1. TLA+ Sets correspond to Types

In Wombat2 there is a lattice hierarchy of types that make them behave quite like sets. In TLA+ there are no types, but the way he uses sets, such as the set of Integers, corresponds closely to wombat2 types.

Lamport also claims that "everything is a set" using the ZF (Zermelo-Frankel) system. So 3 is a set, and maybe 2 is an element in 3. Such nonsensical questions don't arise in Wombat2. Yes, you could use ZF as the implementation of natural numbers, but that doesn't make properties of that implementation into properties of the type being implemented. This doesn't cause any conflict between TLA+ and wombat2 because TLA+ doesn't make any substantive use of this.

2. TLA+ mapping corresponds to Proc

On page 14 he talks of "mapping", giving * (multiplication) as an example that is defined for numbers. Since there is no type system to exclude non-numbers, we presume the mapping fails for non-numbers. And so this corresponds to Proc.

A mapping that always gives a boolean result is called a "predicate". This corresponds to a TProc(X,Bool). He gives "=" as an example, and in Wombat2 "==" is also defined for any pair of values.

3. Expressions and Formulas, meanings and interpretations

Numeric expressions using constants and arithmetic operations are distinguished from Boolean expressions, also called formulas. These exist in wombat2, of course.

Then on page 15 we see algebraic expressions and algebraic formulas. These have "variables" in them. Wombat2 reflection allows looking inside expressions. Identifiers and operators, which are compile time things, get converted to atoms which are runtime things. Wombat2 is more general, since Lamport is only talking about numbers. TLA+ writes the meaning of any of these with special (doubled) square brackets: ⟦exp⟧. Then an "interpretation" is a mapping from variable identifiers to values. In wombat2 the equivalent would be a record type mapping atoms to values. If ϒ is an interpretation in TLA+ then ⟦exp⟧(ϒ) is the value of the expression with that assignment of values to variables. Wombat2 can do something similar, but it is only in a part of the language not meant for ordinary programming.

Formulas are also similar to wombat2 proposition types. These are types that correspond to a a proposition, with a value of the type being a witness. 

4. Subsetting corresponds to subtyping (including refinement/subset types)

TLA+ { x∈X | F(x) }, for some formula involving x, corresponds in Wombat2 to X/{ F%($) } where F% is a Type expression with an input argument of type X, and where values of X are included if the generated type has a value (witness).

5. Mappings and Functions

In TLA+, mappings have 0 or more untyped arguments. The defining expression may be only valid for arguments from some "sets". Mappings can cover things that are too big to be sets. In wombat2 things too big to be types are in a higher universe, but I haven't worked out how that exactly works, but currently there is no similar distinction.

A function in TLA+ has one input, that can be a tuple, and one output, which can also be a tuple. So corresponds pretty well to TProcs in wombat2. Where TLA+ writes v∈S↦exp, that corresponds to {'S=>T: `v=$; exp }. Functions(=TProcs) are values just like numbers in TLA+ and wombat2.

6. Lists, Tuples, etc

TLA+ has lists (in angle brackets) that are "ordinal sequences. Ordinals are "first, "second", etc. So TLA+ has indices starting at 1 so that the second item is item 2. Then it has ordinal sequences that are meant for things that happen starting at time 0, so these are 0 based, and the entries are separated by right arrows: →. The latter seems to correspond to the semi-colon separator between effects in wombat2.

7. Rendering effect-based programs as mathematics

We then come to the parts of TLA+ that are used in proving things about programs. This is the stuff that wombat2 would like to learn from.

The first trick is to divide the execution into steps. Then each variable turns into an array of values, giving the value at each step. Then the execution of the program can be expressed as logical facts about how these variables have values at each step. Wombat2 has a start in this direction with the TimeOrder values marking the start and end of effectful expressions.

Logical operations in TLA+ are extended with "always" (▢) and "eventually" (◊) and "always eventually" and "eventually always".

The Lattice Type System

I'm making very bad videos. Here's an intro to wombat2:

Here's the the one on wombat2's type system:

Proposition types complement subtyping

The way wombat2 works, both at compile time and runtime, is that actions are taken to move an expression's known type down the hierarchy. When we get to a type restricted to a single value then we have evaluated the expression. When we get down to a type restricted to the empty set of values, then expression evaluation has failed.

A natural question is: why do we have types representing propositions, such as:  x <% y. Why not just simple boolean expressions.

Suppose we have a type Dog, and it's a subtype of Animal. We have a value x of type Animal, and we have some proposition about it: say hasTail(x). Moving down the subtyping hierarchy can't invalidate a witness of this, or a witness of its negation. But if we can't decide until we've moved to a more specific subtype then the proposition and its negation both stay empty. Propositions can be evaluated at the right level of generality.

Wombat reborn ... as Wombat2

 I've decided to bring back the wombat name. Except that it is now wombat2 - no space before the 2. This will hopefully be easier to search for.

Future posts back at https://wombatlang.blogspot.com/.

Also: I've started posting videos on my PLodicy youtube channel: https://www.youtube.com/@RobertSmart/.

The Ken Programming Language is Wombat's successor

 See: https://ken-lang.blogspot.com/2023/06/ken-has-spec.html.

Behaviours, Bases, Modes and Properties

Behaviours, Bases, Modes and Properties

[This is just a copy from this docs file: https://docs.google.com/document/d/1wJoLRP9bV70d7bL_JNF2pk7U0cvHQ1lNevDOI09FDG8/edit?usp=sharing. I finally found a reasonable way to move docs to blogger: export as html, open that and copy-paste into blogger.]

[I plan to change the name from Wombat, perhaps to Emmy, in honour of Emmy Noether]

The term "Type" is overloaded, with some saying the values can only have one type, but others allowing subtyping, so that values of a subtype are also of the higher type. To avoid this confusion, and also because both concepts are needed, Wombat has two separate notions:

• Base. Every value belongs to a unique Base. Bases are organized in a partial order by the isA hierarchy. For example Integer isA Rational.
• Mode. Every value has one or more Modes, as described later, and they form a complete lattice, based on the isA hierarchy. This is what user level programmers normally deal with, supporting common sense notions such as: if g is a Group then it is already a Monoid, and it doesn't need to be converted.

Bases

All values have a unique Base. Programmers usually deal with modes rather than bases, since they support subtyping (submoding).

There are primitive Bases which come from the compilation target. For example if the target is Amd64, then Int64 (the type of 64 bit Integers) might be a primitive Base with properties derived from the hardware manual.

All other Bases have one or more implementations. The implementations need not be primitive, but there can only be a finite chain of implementedBy before getting to primitive Bases. At run time all values are of a primitive Base.

Bases are characterised by properties (which come bundled in Behaviours). Access to values is only through the properties of its Base: peeking at the implementation is only allowed in a controlled way to optimize. The properties of a Base are implemented using the properties of the implementing Base.

Bases are organized in a partial order by the isA relationship (which derives from the reflexive and transitive closure of all isA declarations). For example we might have Integer isA Rational. This definition provides an inverse pair of procedures between the two Bases (the up procedure is total, and the procedures are inverses).

When two Bases are linked by an isA relationship then any properties they both have must be compatible. This means that the values must be combinable, as explained in a later section. A Base inherits properties that it doesn't already have, so that, for example, Integer will inherit the denominator property from Rational.

There can be indexed families of Bases. For example List is indexed by Base, so for any base X, List X is another Base.

Necessary rule: all chains (totally ordered subsets) of Bases must be finite, so they have a maximum and minimum element. For example we couldn't have: forall X: X isA List X, because that would create an infinite chain with no maximal element.

We also have the rule that a base can only have a finite number of bases above it and below it in the hierarchy. This is necessary to make combine work -- see below.

Properties and Behaviours

Values known at compile time can have properties, which are simply named values.

Properties are always defined in a bundle, called a Behaviour. A Behaviour specifies what Base of value it can apply to. For example the monad behaviour can apply to a base=>base. We are mostly concerned with the properties of Bases, and how that translates to the properties of Modes.

[Of course the isA PO on base induces a PO on base=>base, but I don't know how all this can be generalized to such induced POs.]

A property is characterised by (a) the Behaviour it comes from; (b) the name (an Atom); (c) the how index (since a value can conform to a Behaviour in more than one way). The same property can apply to multiple Bases in the Base hierarchy, but when it does it is required to be consistent when one is above the other in the hierarchy. For example the ".add" property is required to be compatible between Integer and Rational. [Well actually it is the .binop property from behaviour CommutativeGroup with how index .add.]

Behaviours are also organized in a hierarchy that is a lattice by extends.

Modes

Modes are based on Bases, but add subtyping (which might be called submoding, but I won't). We create the Modes as follows:

• For each isA-antichain, i.e. set of noncomparable Bases (no member of the set is above or below another) (includes the empty set and singleton sets), we create a Mode: Union(anAntichainSetOfBases). We also define Intersection(anAntichain) by finding the maximal elements of the set of Bases that are below (or equal to) all Bases in anAntichain and taking the Union of that (and Intersection of the empty antichain is the top Mode: Any).
• We then define an ordering on Modes Union(sb1)<=Union(sb2) iff every Base in sb1 is <= some Base in sb2 (in the Base isA hierarchy).
• Given two Modes: Union(sb1) and Union(sb2) we see that there is a sup which we get by taking the set union of sb1 and sb2 and eliminating any element that is less than some other element. To get the inf we define Intersection: we take the set union of sb1 and sb2, eliminate non minimal elements and take Intersection of that antichain.
• So Modes form a lattice with Empty=Union([]) at the bottom and Any=Intersection([]). Empty has no values, Any has all values.
• Bases convert to Modes automatically (convertsTo relationship): X->Union([X]).

Values belong to multiple Modes. If a value, v, has a particular Base, B, then it belongs to the corresponding Mode, and also every Mode above it in the Mode lattice.

Modes have properties derived from those of Bases. Every property of a Base extends to the corresponding Mode, and also to every Mode below that which doesn't already have that property (if it does have the property then it is required to be compatible).

Compatibility (combine operation)

Firstly we note that if a procedure isn't surjective/onto, then for many purposes the output type might as well be Any. And for partial functions, which may fail for some values of the specified input type, then for many purposes the input type might as well be Any. While this is arguable, it does make it easier to talk about the following, and we will only be considering partial procedure types of type Any=>Any.

Distinguishable is a Behaviour, and Bases that conform to it support equality (= op for our purposes). A weaker behaviour is Combinable which defines the combine operation. For types that support equality, combine checks that the values are equal, and returns that value if so (otherwise failing). The most important Base that doesn't conform to Distinguishable is procedures. But they also support combine is the following way:

• Given 2 procedure, f and g, we create a new procedure c=combine(f,g).
• When c is called it passes the input to both procedures, and the result it returns is formed by combining the output.
• If one procedure fails, then the result of the other is used.
• If the outputs support equality then c succeeds if f and g return the same result, else fails.
• If the outputs are new procedures (or other Combinable), then the result is the combined procedure (or other).

Combining Properties

We'll consider the Behaviour Add with property .add, defined thus (approximately, leaving out "how"):

`Add = newBehaviour Base {$=`B:Base; `M=B:Mode; struct [
                                                .add->(M*M)=>M
                                              ]}; ...

Integer conformsTo Add by { struct [ .add->integerAdd ] };

Rational conformsTo Add by { struct [ .add->rationalAdd ] };

Integer isA Rational by (integerToRational,rationalToInteger);

Integer can't inherit .add from Rational, because it already has it. What happens, to prove compatibility, is that the two .add procedures get combined into one. Here's how that works:

• If the input is 2 integers then integerAdd succeeds returning an integer, and rationalAdd succeeds (after the parameter gets converted to 2 rationals), giving a rational. Then the equality test gets called and it forces the parameters to the Intersection or Rational and Integer, which is Integer, where the equality test succeeds.
• If the input is 2 rationals, at least one of which is not an integer, then integerAdd will fail without even being called, and rationalAdd will succeed and give the result.

Now suppose that we have a Base ComplexInt (i.e. Gaussian integer), with .add defined, but that Integer itself does not have .add defined:

ComplexInt conformsTo Add by { struct [ .add->complexIntAdd ] };

Rational conformsTo Add by { struct [ .add->rationalAdd ] };

Integer isA Rational by (integerToRational,rationalToInteger);

Integer isA ComplexInt by (integerToGaussian,gaussianToInteger);

Now Integer inherits different .add from both parents. Once again the solution is that the .add properties are combined. So when two integers are added then: (a) we convert them to rational and add that; (2) we convert them to complex and add that. To check equality we have to force the two results to the intersection (which is Integer) and check equality there. Which succeeds!

Obviously these combined operations are likely to be inefficient. It is expected that all important cases can be optimized, but not necessarily automatically.

So every property (Behaviour-name-how) has a Mode of all types with that property. And all those properties are combined and the same across that Mode. All operators map to a procedural property in this way.

State of play

I haven't made much progress since the start of Dec 18. Hopefully that will change.

I used to put minor stuff in wombatlang google+. That is going away and I'm not sure how to replace it. Maybe I'll post a "small stuff" post at times and put stuff in the comments. For the moment I'll use this post.

Because there is some discomfit with things having multiple types, I intend to use the word "Mode" instead (in deference to Algol68). For a given value, its Type will be the lowest Mode it can have in the type hierarchy (now "mode hierarchy"), without going into subset modes. Note that if you have 2 Modes with an isA relationship between them, but the lower one has no additional properties that aren't inherited from the higher one, then the lower one is regarded as a subset mode, since it is indistinguishable from one.

Nobody (except me) likes the Wombat name, so I'm going to change it. I rather like Emmy, in honour of one of the 20th century's greatest Mathematicians: Emmy Noether. Or I could look for a name that highlights some of the features of the language, such as: closure orientation, type/mode lattice, bidirectional typing and bidirectional execution driven by the type/mode lattice: BiCLat. Suggestions are welcome to robert.smart@wombatlang.org.

In https://golem.ph.utexas.edu/category/2019/03/left_adjoints_between_categori.html, John Baez makes a push to call "bounded lattice" just "lattice". I like this: there doesn't seem any reason for lattices that don't have a top and bottom, and these can be easily added if missing. However I probably will want sup/inf of more than finite sets: at most "computable sets". So somewhere between lattice and complete lattice. Anyway I'll just say "lattice" from now on.

post-talk plans

The talk was not one of my best. I do this thing where I get the talk to a usable level quite early, planning to improve it. But then the thought of changing it makes me nervous. It could have done with animations and better use of the presentation hardware, and more planning to leave room for the interesting stuff at the end.

I've decided to give up on space as the separator in explicit Lists, though cute. So comma is always used for operations that create a compound value, overriding the comma operator that creates Tuples.

Had an interesting discussion of subtyping and equality. I can see that it is useful to also have a system where you take a type and add some extra data and methods, and have a forgetful procedure/coercion to go back to the original type, and some automatic inheritance of properties. However I'm wary of introducing the confusion that eventuates in OO where parent and child have the same property with different meanings, e.g. equality.

Another interesting discussion with the guy advocating weak algebraic effects. That only works with left to right evaluation. Haskell was forced to monads because of lazy evaluation. I hope to avoid that with the TimeOrder type. To reduce the need for !s I will introduce EffectfulProcedures (`!{ }) which force left to right evaluation (i.e. calls to them have an implicit ! unless there is an explicit one).

I was disappointed not to get any useful discussion on proofs.

I'm preparing two docs: Wombat Tour and Wombat Operators to cover my ambitious implementation plan.

Upcoming talk, compiler runs real programs

I'm giving a talk at SAPLING18 which is an informal meeting following http://aplas2018.org/. See at the bottom of the "tracks" menu, but the link is down as I write. I have preliminary "death by powerpoint" slides https://docs.google.com/presentation/d/1a72bKhCxfNBj7lqPVWfqLPDW_QPgQEKy7N0LM8RCo0o/edit?usp=sharing. Hopefully they'll be improved for the actual talk. I'll also be at the main conference. I'm shy, but happy to talk to anyone. I'll also be there on the Saturday before the meeting if anyone wants to have coffee or some such. My email is robert.kenneth.smart@gmail.com. To finish off wombat I need an effects system, and a proof system, but I'm happy to talk about any other aspects of programming language design.

I'm happy to give Wombat-related talks in Australia. I did give one last year at the Melbourne FP meetup: https://www.meetup.com/en-AU/Melbourne-Functional-User-Group-MFUG/events/zhtdllywkbjb/. An attendee was disappointed that there was no code to play with. That inspired me to write the current compiler which now correctly runs some programs, such as factorial:

%/include wombat.wh

    `fact = { case $:Nat of [
                { $ = 0; 1}
                { $ = `n; n*fact(n-1) } # n-1 fails if n==0
              ]
            };
    print (fact 4)

And it can even run simple programs backwards, though not factorial. Check it out from github: https://github.com/rks987/marsupial. (cd src; python3 compiler.py test.w)

Effects and Proofs

Running procedures backwards is nice at times, particularly for matching in case statements. However it is only going to work when there is no information loss (procedure is 1-1), and most complex procedures aren't. I think I know how to run more complex things, like factorial, backwards (to stop arms of a case going into infinite loops you run the cases in coroutines, and when one succeeds kill the others and restart them with the improved parameter). However that will very rarely be useful. The current scheme probably hits the sweet spot in usefulness.

So I should move onto more important things: Effects and Proofs.

My simple-minded idea of effects is that they arise in types where the semantics includes the time. For example an Assignable(X) has a stream of assignments with associated times, and a stream of accesses with associated times, and the semantics specify that the result of an access is equal to the value of the most recent assignment. Similarly IO operations typically need to be done in some order (not necessarily linear: some can be done in parallel). The plan is to provide a framework for this, but leave any specific cleverness to the types themselves (and their related operational properties).

First we introduce a new (special) type TimeOrder. This always starts as a future time, then turns into an actual time when passed. Time related operations use the ! operator. There is also !< and any other time related operators should include an !.

• `t ! expression means that the expression should happen at TimeOrder t. This is infix !.
• ! expression allocates a nameless time. This time specifies that the expression is executed in lexical order relative to other ! expressions in the current closure. This is prefix !.
• t1 !< t2 means that t1 must happen before t2.

So consider:

`t1 ! expr1; `t2 ! expr2; `t3 ! expr3; t1 !< t3; t2 !< t3

This says that t1 is before t3, and so is t2, but t1 and t2 can be in either order (or concurrent). TimeOrder entities can be passed around like any other. If a call to a procedure is not done with a bang (!), then, even if it has IO or other effects internally, it will be treated like any other expression and may be executed in any order or not at all.

It is not yet clear whether this simple treatment can be used by libraries to achieve the control of effects that we are coming to expect.

The next issue is proofs. I need proofs, and it seems that the language should be well designed to allow them, but I can't seem to figure it out.

Propositions are dependent types which are proved by constructing an inhabitant. Wombat supports dependent types and uninhabited types. Proofs are programs, i.e. procedures. That shouldn't be a problem.

Let's suppose that a % sign indicates a proposition as a type. Let's consider 1 <% 2 (natural numbers). This type is inhabited. Maybe it is useful to think about what the inhabitants are like and what relation they have to each other. Proofs are programs, meaning a closure in Wombat. So I guess it takes no input and generates an object of the type. Suppose we have some builtin stuff (axioms):

• zeroLessThanNonZero takes n:Nat and returns an element of the dependent type 0<%n.
• moveLessUp takes an n<%m and return an element of type succ(n)<%succ(m).

Now our proof of 1<%2 is { 1 |> zeroLessThanNonZero |> moveLessUp } where x|>f means f(x).

Now suppose we have a proposition "for all abc there exists xyz such that prop(abc,xyz)". This also has a (different) procedural view where forall corresponds to input and there exists corresponds to output. That should suit Wombat where we access to both in the body of the closure. So first of all we have something like: { $=`abc; `$=`xyz; code-generating prop(abc,xyz) }. Then we have to turn that into a proof. We must be pretty close.

Compiler works (minimally)!!!

Version 0.0.1 of marsupial/wombat has successfully run on one specific program ("print 42").

At this point I should say a lot more and there should be docs, etc. But all that will have to wait.

The code is at: https://github.com/rks987/marsupial

The next version, 0.0.2, will aim to run the factorial program backwards. Then I'll retire unless I find some collaborators.

The compiler is in python 3. All the bugs would have been found by type checking. [Update: 0.0.2 development have revealed a few "real" logic bugs, but I certainly plan for the actual compiler to use python type-checking.]

The Bounded Lattice Type System

I've written a little doc on the Bounded Lattice Type System (BLTS) that I'm trying to implement. The pdf is at https://drive.google.com/file/d/1j8JkphjBrTrx-WrQPNbO8VlC2wIE8uSK/view?usp=sharing. This comes from the google docs doc: https://docs.google.com/document/d/1fSxGKq5aD7BMOUGJwH0_jkvVi6w1doRXldDIgJISSWQ/edit?usp=sharing. This is an uglier version:
[[UPDATE: The pdf and docs versions above have been fixed [see comment below]. This hasn't been, may never be.]]

The Bounded Lattice Type System

The Bounded Lattice Type System (BLTS) is at the core of the programming language I'm (slowly) working on. This is an attempt to extract a description of just the type system.

The whole thing fits together like a jigsaw (or sudoku) puzzle. You might think that you like some bits and not others but I strongly suspect that it is not possible to change the core ideas without it falling apart. It took years to get to this current point, and it was only well after the last fix that I noticed that there were no more nasty interactions (that I know about).

In the types of Type Theory, elements can only have one type. In BLTS a number can be an integer, and a rational and a Gaussian (complex) integer. An animal can be a dog, and a mammal, and a quadruped.

Procedures in BLTS are not normally total. If they can't return the required result they fail, and this often leads to alternative action. This is informational failure, which is the only sort under consideration in this document.

The Lattice

A bounded lattice is a partial order where every set of elements (including the empty set) has a least upper bound (join) and a greatest lower bound (meet). In BLTS the types form a partial order with the isA relation. So, using the examples mentioned, we have: Integer isA Rational; Integer isA ComplexInteger; Dog isA Mammal; Dog isA Quadruped. The isA relationships always come with a pair of procedures converting up and down. The up procedure always succeeds (for parameters of the right type), but the down procedure naturally fails when the value is not of the lower type.^[1]

Types are characterized by their properties. Properties are monotonically decreasing. If Rational has the property "denominator" then Integer must have that property as well, and they must agree. The meaning of agreement is covered below.

The join and meet in BLTS are Union and Intersection. Union of the empty set (of types) is the type Empty which has no members (is uninhabited). Intersection of the empty set is the type Any (Union of all types). Union(X,Y) has values which can be either an X, or a Y, or both if they fall in the Intersection. So given xy:Union(X,Y), one can ask if it's an X with xy:X, or if it's a Y with xy:Y. Proponents of parametricity will say that these are the only properties there should be. However we'll see that that is not the case in general in BLTS.

To find Intersection(X,Y), find the set of types directly (immediately) below both, and take the Union of that set. The asymmetry between the definitions of Union and Intersection is, I think, illusory, and I believe these rules give the free bounded lattice that contains the partial order generated by the transitive closure of the isA relationships. Confirmation or disproof of this would be welcome.

Combining

This is going to seem like a strange detour, but actually it is a key solution to various problems.

BLTS utilises a procedure, caseP, which performs the function of a case/switch statement. It is curried. The first parameter is a set of procedures (actually a bag, but repeats won't change the result). This is like the arms of a case statement in other languages, except that the match tests have moved inside the procedures. The result of caseP is a procedure which takes a parameter, and passes that parameter to all of the procedures in the provided set. The common expectation is that one branch will succeed, all the others will fail, and the final result is the result returned by that successful procedure. However if two (or more) procedures return the same result then that is ok as well.

But what if the results returned are of a type that does not support equality (does not conform to Distinguishable). In this case we allow a weaker condition: Combinable. If a type supports Combinable then there is a property 'combine' which allows 2 or more of that type to be combined. In particular, procedures are Combinable. For types that support equality the combination is the value if all are equal, else it fails.

For procedures the combine procedure takes a set (bag) of the procedures to be combined and passes the parameter for the combined procedure to each of the procedures being combined. If the results are Combinable (includes Distinguishable) then the result is the combine of the results of the successful procedures. Yes that's right: the combine for procedures is precisely caseP.

That was a surprising result, but then caseP started turning up all over the place.

Properties

Properties are not duck typing. All properties come from Behaviours (spelt with or without the 'u') which are collections of properties and the laws they must obey. One aspect of agreement between properties is that they come from the same Behaviour.^[2]

Suppose we have the property 'add' from the Behaviour 'Monoid', and both Integer and Rational conform to Monoid. The isA relationship has the effect that the two 'add' implementations are combined  for both types. If the parameter to add is a pair of Integers then both of the combined original procedures succeed, and the results are checked to be equal. If the pair contains a non-Integer Rational then the 'add' property of Integer will fail, and the result will come from the 'add' property of Rational just as before. So the only effect of combining them is to check the compatibility. One would naturally hope to optimize this away most of the time.

We note that properties must be of a Combinable type. This is not expected to be an onerous restriction. Combinable is inherited in all standard types, so that, for example, a Tuple type whose component types are all Combinable will be Combinable.

Diamonds

Suppose we have defined a ComplexRational type giving the following diamond problem:

As we go up our partial order, our transitive closure generates the obvious induced up and down procedures. But what happens when we have a diamond as in the diagram. We require that both upward routes give the same induced up and down procedures. I'm sure you're ahead of me. Naturally we combine them, which ensures that when both paths succeed they give a compatible result.

Properties of Unions

Consider Union(Rational,ComplexInteger). If no types have been declared above Rational and ComplexInteger then the 'add' property is not defined for the Union. But now suppose we have defined ComplexRational with the obvious isA relationships, as above. For Union to give the join we must have:

The Union must be below ComplexRational. We construct the up and down arrows in an obvious way with combine^[3]. But ComplexRational supports the add property, so everything below must also, including the Union. However it just inherits ComplexRational's add, and doesn't make the Union itself a monoid (which is good because it isn't).

To understand the value of this, consider the list [7,8/3,2+5i]. It is naturally a list of the Union of the types which is Union(Rational,ComplexInteger). If we sum the list we want to get a ComplexRational if that is defined.

Why don't we just say that ComplexRational is the Union of Rational and ComplexInteger? The answer is that there might be multiple types above both Rational and ComplexInteger. Let's add the type Cat with Cat isA Mammal and Cat isA Quadruped, and consider the list [cheshireCat, snoopy, pluto]. If forced to make a premature decision it would be a List( Mammal) or a List( Quadruped). But by making it a List( Union( Dog, Cat)) it isA either of these if that is required.

Which brings us to another interesting point. What is the type of the empty list, []. Since the type of an explicit list is the Union of the set of types in the list, and since the Union of the empty list is the type Empty, we see that [] has type List(Empty). And since Empty isA X for all types X, we have (with reasonable assumptions about active declarations) that List(Empty) isA List(X). Which is exactly what you want to be able to use the empty list in any appropriate situation. I prefer this to the way the empty list is handled in other languages.

No home types

If x is both an Integer and a Rational, there is no sense in which we can ask "Is x really a Rational with denominator 1, or is it really an Integer". If this were not so then the programmer could encode hidden variables in that type information which would be most undesirable.

Out of Scope

Tuples (product types) are also used heavily in my language. Naturally the 0-Tuple is Unit. There is much more, but it is not closely connected to the lattice nature of the type system and the role of combine. So I should stop here for today. But I can't resist one more diversion.

Implementations of Types

All types are either primitive or implemented in terms of some other type. So the full Nat type of natural numbers might be implemented using List(UInt64) where UInt64 is a primitive type of 64 bit unsigned integers provided by the target hardware, and List types might be implemented using various possible primitive interfaces to memory. This "implemented by" relationship has absolutely nothing to do with the isA relation.

Primitive types could arise in various ways. One that mathematicians seem strangely fond of is the type of hereditary (pure) sets which in ZF(C) set theory are sets whose only members (if any) are other hereditary sets. It is possible to implement a model of the natural numbers with such sets. But this is an "implemented by" situation. There should be no suggestion that the natural numbers are such sets. Rather the natural numbers are defined by their properties: zero and successor, and laws governing those. To know that you've implemented the natural numbers you need to define the properties and prove the laws of natural numbers using the properties and laws of the type with which they are implemented.

---

[1] These procedures don't change the types of any values, and seemingly don't do anything other than failing at times in a downward direction. In the practice of an actual programming language there is a meaningful interaction with the implementations of the types.

[2] A type can conform to a Behaviour in more than one way. The different ways are indexed by some type that supports equality. Properties are thus specified with a Behaviour, an index and a property name. We will ignore this subtlety.

[3] The up arrow is the combine of (1) down to Rational and up to ComplexRational, with (2) down to ComplexInteger and up to ComplexRational. We see that this must succeed one way or the other (or both if it is an Integer). Down works the other way and will fail iff both initial down movements fail.

code for Wombat/Marsupial Operators

[Update: This was an insanely premature announcement. Stay tuned ...]
[Update2: now looks roughly ok -- next step write an interpreter]

One of Wombat's many aims was to have user-defined operators that are so good that there is no need for operators to be built into the language at all.

• Parentheses ("(...)") are just an operator with no left and no right that maps to the identity function.
• Semicolon ("statement1;statement2;expression") is an operator: with left and right and low priority on both sides.
• etc -- operators are the only syntax for most users.

We now support different versions of an operator with a left or with no left (e.g. x-y versus -z). Also operators overlap as long as they stay the same until they diverge by either a (mandatory) operator or by whether a mandatory operator is/isn't followed by an operand. E.g. "[" has 3 forms:

• [ ] is the empty list
• [ space-separated-elements ] is an ordinary list. Note that wombat uses space as a separator here, so procedure calls have to use adjacency f(x) or be parenthesised (f x). You don't like that? It's really trivial to change operators, and still be compatible with other code.
• [ head | tail ] intended for pattern matching, but works either way.

The point is that both the compiler and the reader can understand which is which with only one token lookahead.

The code for this now passes the barest one line test. I'll get back to testing it when I have more wombat code. The code is in v0.0.1 under marsupial (https://github.com/rks987/marsupial/tree/v0.0.1). Marsupial is just the bare minimum, and the plan is eventually to separate out the include/import/require files that turn marsupial into wombat.

If any languages out there would like a comprehensive scheme for user defined operators then I might find time to help. It is written in python3, but really just uses json-level features (apart from using generators), so I think it will fit into other languages. The problem is interacting with compiler defined operators already there. Wombat doesn't have that problem because there aren't any!

No Holes in Closures, and "case" behaviour

No holes in closures

In Wombat closures are the only block structure. So closures are often called immediately that they are created, and it is easy to forget that they are potentially independent entities. In particular it is clearly wrong to allow references to external identifiers to refer to ones which are still holes and don't have values at the time of closure creation. For one thing the closure will run differently before and after the hole is filled.

Holes should only be passed to closures at closure execution time, via the input parameter ($) and the output (`$). So the code for the appendTest example (from Logic Programming in Functional Style) should be:

`append = { # $ is 2 input lists

case $ of [ # nb. "case x of y" just maps to "caseP y x" { $ = ([],`y); y } { $ = (`hdx +> `tlx, `y); hdx +> append(tlx,y) } ] }; print( append([1 2],[3 4])); # [1 2 3 4] [1 2 3 4] = append([1 2],print(`a)); # [3 4] [1 2 3 4] = append(print(`b),[3 4]); # [1 2]

 And the code for the factorial example (from Quantum, Entropic and Entangled computation) should be:

    `fact = { case $:Nat of [
                { $ = 0; 1}
                { $ = `n >? 0; n*fact(n-1)}
              ]
            };

    6 = fact `x; print x

Case Behaviour

Another problem in the factorial example is that the 2nd option won't terminate without substantial and inappropriate compiler cleverness, as the rules stand. I could use firstCase instead, which would work in this particular example, but it is a hack (even though it is the only case construct in most languages). So my current thinking is that when running backwards and matching the output instead of the input it should act like anyCase and abort other branches when a match is found. But I don't think that is quite the right answer.

Quantum, Entropic and Entangled computation

[See the new post https://wombatlang.blogspot.com.au/2017/06/no-holes-in-closures-and-case-behaviour.html for fixes to problems in this post.]

In the quantum world every event is reversible. But above that we have the world of everyday experience where entropy always increases, time moves relentlessly forward and events are not reversible.

In computing there is a similar situation. Some functions don't lose any information when run in the normal forward direction, and these should be able to be run backwards to give the inverse function. Factorial is such a lossless function, and it is interesting to run it backwards in Wombat. [Relevant aspects of Wombat are given at the end for newcomers].

`fact = {   $:Nat = `n;

           caseP [

               {n=0; 1}

               {n>?0; n*fact(n-1)}

           ] ()

       };

6 = fact `x; print x

• `x = H1 -- call fact (Holes are given as Hn, as they are created).
• in fact for the 1st time. $=n=H1. `$=6.
• in 1st case n=H1=0, `$=1 fails
• 2nd case. n=H1, 6=H1*fact(H1-1)
• in fact 2nd time. $=n=H2=H1-1. `$=H3. 6=H1*H3.
• in 1st case. H2=0. H1=1. H3=1 -- 6=1*1 fails
• 2nd case. H2>0. H1>1. H3=H2*fact(H2-1).
• in fact 3rd time. $=n=H4=H2-1=H1-2. `$=H5=fact(H2-1). H3=H2*H5. => 6=H1*H2*H5
• 1st case. H2=1. H1=2. H5=1. But 6=H1*H2*H5=2 fails.
• 2nd case. H4>0.H2>1.H1>2. H5=H4*fact(H4-1).
• in fact 4th (and last) time. $=n=H6=H4-1=H2-2=H1-3.
                         `$=H7=fact(H4-1). H5=H4*H7 => 6=H1*H2*H4*H7
• 1st case. H6=0. H4=1. H2=2. H1=3. H7=1. 6=H1*H2*H4*H7 succeeds! The answer (x=H1) is 3.
• 2nd case. Exercise: Prove that result must be greater than 6... fails

As we recurse, we keep creating new holes, and having to remember the relationships between them. This is vaguely reminiscent of thunks in lazy languages. It is also feels like entanglement, though whether it could have anything to do with quantum physics entanglement is left as an exercise for the reader.

---

some relevant features of Wombat are:

• An identifier is preceded by backquote when used for the first time. It starts life as a hole, and like all holes it can only be filled in once. `x:Int; x=3 (Explicit typing is optional.);
• An explicit procedure (closure) is just an expression in braces -- { x+1 } ;
• A closure's input is $ and its output is `$. The input is commonly a tuple which is unpacked immediately, and $ is never mentioned again -- { $ = (`x,`y); x+y } ;
• If `$ isn't explicitly unified, then it is unified with the whole expression: {$+1} means {`$=$+1}.
• For each boolean operator, there is a version with ? (such as >? above) which succeeds or fails, instead of returning true or false. The failure is informational, allowing alternative paths. A double ? would cause a fatal error when false. The ubiquitous = operator is the same as ==?.
• caseP takes a list of procedures, passing the 2nd parameter (just () above) to each. It expects exactly one to succeed, giving its result. Actually more than one can succeed if they give the same or compatible results, but that's another story. The example above would have been easier if I'd used firstCase instead.

P.S. I fixed the formatting in the previous post. Don't ask me how Blogger corrupted it.