Backquotes and Iterators

One of the intended features of Wombat was to firmly disengage names from values. The process of incorporating holes into Wombat revealed that I’d got it wrong. I want to use a backquote (`) prefix to mean “this is a new name, unrelated to any outer use of this name”, but also to indicate that this was a hole waiting for a value. As always, any such confusion between names and values causes things to not fit together. Here is the new syntax:

The backquote introduces a new name and is only used on the first appearance of that name. This also applies for free variables. For ordinary variables the scope extends to the end of the current explicit closure or current file if at file level. For free variables it just extends to the the next use of backquote on that name. This allows reuse of free variable ids, which is something mathematicians do a lot.

When the thing being defined by unification is the result of a function call then there is a separate hole for each possible input value. So we can add unifications for other input values as long as they are compatible:

   `fact 0 = 1;
   fact 1 = 1;
   fact (`n:Int >? 0) = n * fact (n - 1);

The 2nd line is redundant, but harmless. The 3rd line implicitly contains

   fact 1 = 1 * fact 0;

But since both left and right sides are already defined, it is just a check.

If you have mutual recursion, you just put the backquote on the forward reference. The fact that it starts out life as a hole doesn’t matter as long as it is filled before its value is needed. This allows forward references in procedures defined in the multiple pattern style shown here for fact. This means the first occurrence at the same level. Forward references in inner explicit closures don’t need and shouldn’t have a `, and indeed putting one there would create a new and different name.

Every value starts out life as a hole and acquires a list of unifications that it has to satisfy. A hole can only be filled once - it is not a mutable value. Every time a hole gets filled then all the unifications that are associated with that hole are rerun and either resolved or updated to have that new value instead of the hole. So:

   `x + 1 = 7 # sets x to 6
   `y + 1 = `z # guaranteed relation between x and y
   z = 42 # resolves z and y

Once a hole is filled it has a value and a type.

Note that you can put new names separately, with optional constraints, and not use backquotes in actual expressions.

   `x:Int;
   x + 1 = 7 # sets x to 6

---

Iterators

Iterators are nice, but I didn’t want to introduce them without sticking to the “everything is a procedure” plan. Here’s the construct, which replaces the previous use of `{...}. Note that the uses below of backquote in operators `{, `yield and `( have nothing to do with its use for names as above.

A value of type Stream(X) is just a procedure which takes no input (Unit) and returns the head of type X and the tail which is a new Stream(X). At the end it fails non-fatally. Convenient syntax for this is now provided:

   `{ … yield expr … }

Creates a Stream(X). Each yield expression returns a head, and the tail part is a “magic” procedure that just continues execution. Note that the yield matches with the lexically enclosing `{ iterator, which will normally be in an outer procedure.

But often we just want to put a bit of a shim around one stream to create another. For this we have `yield:

   `yield {... `( expr ) ...}

The expr will be Stream(X), but `(expr) just gives the head. What is yielded is the result of the explicit closure. When going to the next result it reexecs the whole thing, but advancing all the lexically enclosed streams in `(..). If one of those finishes they must all finish, and then it moves on looking for other yields. [It has to be a closure for repeated execution.]

So to take a list and return a stream of pairs of lists which partition it:

`unappend = `{
   yield ([],$); # first partition is empty list and input list
   case $ of [
       { $=[];} # no yield, will end Stream
       { $=prepend(`h,`t);# prepend should have some nicer syntax like (`h | `t)
         `yield {(`pre,`post)=`(unappend(t)); (prepend(h,pre),post)} ;}
   ];
}

Well it’s not logic programming, but it’s pretty cute. So I think I’ll give up on logic programming.

I think I’ve resolved all the issues that were worrying me, so I plan to implement a first version of wombat with dynamic typing, no attempt at optimization, and built around python3 as the combined compiler/wctl/target. Hopefully I’ll get something onto github some time this year. Implementation will doubtless reveal errors in the design, and I’ll put updates here, and hopefully also write some better documentation.

Logic Programming with New Wombat

In the previous post I introduced the idea of negative types which are the type of holes. The most common way to introduce them is by backquote-identifer:

`three = 3

Here `three has inferred type -Int, and the hole is immediately filled, giving meaning to three.

Here is a classic logic programming predicate from the Mercury language:

append(Xs, Ys, Zs) :-
( Xs = [], Zs = Ys ;
 Xs = [X | Xs0], append(Xs0, Ys, Zs0), Zs = [X | Zs0] ).

The beauty of this is that it runs correctly whether you are given Xs and Ys and want to calculate Zs, or you are given Zs and want to calculate all of the Xs,Ys prefix-suffix pairs to make Zs, or various other options.

Rendering that in Wombat, we assume: that predicate returns unit (hence trailing “;”s) or fails harmlessly; and that a case expressions fails harmlessly if no entry matches (though I think the doc currently says something else); and that prepend does the same as the “|” construct in Mercury:

`append = {
(`Xs, `Ys, `Zs) = $;
case of [
{Xs=[]; Zs=Ys;}
{Xs=prepend(`X,`Xs0); append(Xs0,Ys,`Zs0); Zs=prepend(X,Zs0);}
]
}

We can call this with all arguments as values and it will just be an assertion style check:   

append([1 2], [3 4], [1 2 3 4])

Or we can call it with the 3rd argument as a hole, and it will be filled in:

append([1 2], [3 4], `rslt)

Here Zs gets unified to be the same hole as `rslt. The unification step Zs=prepend(X,Zs0) then fills that hole.

If we have the concatenated result and want the pairs that will give that:

append(`prefix, `suffix, [1 2 3 4])

then we only get the first option with prefix=[] and suffix=[1 2 3 4]. It would be nice to introduce iterators and backtracking to Wombat in a compatible way. However before we go there, we note that it is more natural in Wombat to do this in a way that looks functional.

`listCat = {
(`Xs, `Ys) = $; `Zs = `$;
case of [
{Xs=[]; Zs=Ys;}
{Xs=prepend(`X,`Xs0); `Zs0 = listCat(Xs0,Ys); Zs=prepend(X,Zs0);}
]
}

In the old Wombat, `$ was always the hole that was where the procedure result would go. In the new Wombat it might not be. If the result of the call is being unified with something, then the something becomes the value of `$. Suddenly the semantics of Wombat unification become much simpler. So in

[1 2 3 4] = listCat( [1 2], [3 4])

`$ will be set to the value [1 2 3 4]. Indeed `$ could be a structure with a mix of values and holes:

[1 2 `x] = listCat( [1], [2 3])

This is all a little too good to be true. I’m sure I’m missing something.

Getting back to iterators and backtracking. It can’t be as simple as Python iterators, because each yield has to specify values for all the holes in input and output that the procedure is responsible for. It would be nice if `{ initiated an iterator and one could write:

`listCat = `{
(`Xs, `Ys) = $; `Zs = `$;
eachCase of [
{Xs=[]; Zs=Ys;}
{Xs=prepend(`X,`Xs0); `Zs0 = listCat(Xs0,Ys); Zs=prepend(X,Zs0);}
]
}

And have it create an iterator-like thing that the caller can advance. I fear I don’t know enough to get this right.

[It is an interesting thing how much parallel there is between programming and physics. Holes are a recurring theme in Physics, being places where particles are absent, they often act like particles. Here we have been expanding the role of holes in Wombat and making them behave a bit more like values. Physics also has its Quantum core where everything is reversible and information is neither created nor destroyed. Programming languages can, and possible should, have a reversible logic core. Then, in both physics and programming, we have the real world where things move forward irreversibly with entropy increasing.]