The Wombat Programming Language
Monday, March 18, 2024
The Lattice Type System
Sunday, March 10, 2024
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.
Saturday, March 9, 2024
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/.
Thursday, June 1, 2023
Thursday, April 18, 2019
Behaviours, Bases, Modes and Properties
[I plan to change the name from Wombat, perhaps to Emmy, in honour of Emmy Noether]
- 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
Properties and Behaviours
Modes
- 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]).
Compatibility (combine operation)
- 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
.add->(M*M)=>M
]}; ...
- 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.
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.
Friday, March 8, 2019
State of play
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.
Sunday, December 23, 2018
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.
Sunday, November 4, 2018
Upcoming talk, compiler runs real programs
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)
Thursday, October 4, 2018
Effects and Proofs
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.
`t1 ! expr1; `t2 ! expr2; `t3 ! expr3; t1 !< t3; t2 !< t3This 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).
Thursday, July 19, 2018
Compiler works (minimally)!!!
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.]
Saturday, March 24, 2018
The Bounded Lattice Type System
[[UPDATE: The pdf and docs versions above have been fixed [see comment below]. This hasn't been, may never be.]]
The Lattice
Combining
Properties
Diamonds
Properties of Unions
No home types
Out of Scope
Implementations of Types
Tuesday, December 26, 2017
code for Wombat/Marsupial Operators
[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.
- [ ] 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.
Wednesday, June 21, 2017
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 listscase $ 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
Thursday, June 15, 2017
Quantum, Entropic and Entangled computation
Quantum, Entropic and Entangled computation
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.
- `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
- 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.
Monday, June 12, 2017
Logic Programming in Functional Style
[N.B. There is code. In https://github.com/rks987/appendTest I have hand-compiled the example below to an AST, and written a pretty-printer to check it is right. Next step is to write an interpreter for the AST. How hard can that be :-).]
- 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}.
- A list is given by elements in square brackets separated by spaces. The +> operator adds an element to the head of the list and is invertible.
- print returns its argument.
`append = {
$ = (`x,`y); # 2 input lists caseP [ { x=[]; y } { x = `hdx +> `tlx; 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]
- x is unified with print(`b) and y with [3 4];
- print is called with its `$ set to the hole x, and its input set to the hole `b. Since it is going to have an effect it has to stall waiting for one or other to be filled. If there were any later effects they would also stall, even if ready to go, because of a lexical ordering requirement.
- At the same time caseP is called with input set to unit (=()), and output set to the output of the whole procedure (i.e. [1 2 3 4]) since it is the last expression. Now caseP calls all procedures in its list expecting precisely one to succeed. In this case:
- Closures execute in a sandbox where unifications with holes from outside are tentative and only make it out if the procedure doesn't fail. If the outside hole gets filled in while the closure is executing then the unification is made firm if it agrees with the tentative binding, or the closure fails if it doesn't.
- So when we look at the first procedure in the caseP, it tentatively unifies x with [], then tries to unify y=[3 4] with `$=[1 2 3 4]. This fails, so that closure fails.
- At the same time we start the more complex 2nd closure. The first line creates a relationship between the 3 holes: x, hd and tl. The 2nd line then unifies [1 2 3 4] with (hd+>append(tl,y)). this sets hd=1 and unifies [2 3 4] with append(tl,y). So we call append recursively with `$=[2 3 4] and $=(tl,y).
- The following time that append is called we have `$=[3 4] and then the first closure succeeds (while the 2nd fails), so that when it returns it establishes its parent's y as [3 4], tlx=[] and hdx=2. This resolves the previous line giving x=[2].
- When this returns the output of print(`b) is unified with [1 2] which in turns sets b to [1 2] and allows the print to proceed.
- If we weren't going to use b subsequently we could have just written print(_) because _ is always a new hole.