Holes: ideas and puzzles

[note that holes have been brought in to version 0.0.4 of the doc, but in a simpler way than this.]

An example from the overview:

firstCase someExpresion of [
{ `x, ok = $; … }
{ `x, error(timeout,`extraInfo) = $; … }
{ `x, `otherError = $; … }]

The idea is that when the error is a timeout we extract the extraInfo and do something with that. The error identifier is acting as a procedure here, and maybe it is one, just building up an appropriate structure:

`error = { (`errorCode,`extraInfo) = $; (.error, errorCode, extraInfo) }

Here we return a 3-tuple with an atom first component used to identify it as an error structure. This might not be a very likely methodology, but it is conveniently illustrative.

`extraInfo is a hole waiting to be filled. What can we make of it being a part of the parameter we pass to error? And holes naturally appear in other places (such as pigworker’s amazing derivatives of data structures). And we’ll see others below. We want to handle them in a uniform way.

The easy thing, if we can make it work, is to see holes as just another type. Let’s write -T for a hole of type T. If X convertsTo Y, then we see that -Y convertsTo -X. If Int convertsTo Rational, then a hole for a Rational can take an Int. We want this to also work for the more important isA relation, and let’s assume that before getting to how it might work.

Extrapolating wildly based on our notation, it is natural to assume that Empty = -Empty, and the other hole types are below that, with -Any at the bottom.

An interesting thing happens when you consider the type Assignable(X) of mutables that can hold a value of type X. Naturally Assignable(X) convertsTo X, so that we can conveniently use the value. But now we see that we can also have Assignable(X) convertsTo -X, which will allow us to use our Assignable as a hole and assign new values using more general hole-oriented code.

The isA rule is that properties must always decrease as we go up. To fit this in we will say that holes types have negative properties. Some types (such as Assignables, or the tuples we looked at above) have mixed positive and negative character. The isA rule now says that, as we go up the isA hierarchy the number of positive properties must go down, while the number of negative properties must go up.

I’m not sure if this is all going to work, but it is fun.

[update: This suggests that an explicit closure should be an Any=>-Any, and maybe other things.]

[upupdate: A cute thing, if this all works is the ancient assignment statement becomes:
someHole := someExpression
and this works in all hole contexts, and its use for Assignables becomes a special case.]

procedures: - combining and adjoint pairs

After the previous post, I feel a need to put things on a slightly firmer footing. This is a start.

Combinable

We define a Behaviour Combinable with a property combine that is a procedure of type SemiSet X=>X. Informally (ignoring side effects):

• Every type that is Distinguishable is Combinable. The SemiSet is a Set if X is Distinguishable. If the set has one element then return it, else fail.
• Procedure type P=>Q are combinable if Q is. The result of combining them is a procedure which runs all procedures and returns the combination of the successful results.
• A Union is combinable if the alternatives are. If the parameters are in one branch only then it is the combination in that branch. If the values are all in the intersection of 2 or more branches then that intersection must support combining (since properties are lost but not gained as we go up the isA hierarchy).
• A tuple with combinable component types is combinable: just combine each component separately.
• Etc.

All types considered in Wombat documentation to date are Combinable, and types which aren’t Combinable will have poor semantics. For example we could imagine a well behaved form of approximate numbers which are defined by a range of Rational numbers. We could say that two are Combinable if their ranges overlap, in which case the combine operation creates a range covering both ranges. But standard floating point numbers are not going to be Combinable in any sensible way.

AdjointPair(X,Y)

These used to be called inverse pairs. That was misleading because it suggested symmetry between the two directions. The new name is also slightly misleading, suggesting that it can be seen as an example of adjoint functors from Category Theory, after which it is named because it seems similar.

If ap is an AdjointPair(X,Y) then it has 2 procedures:

1. ap.to:(X=>Y) never fails for an x:X, and is effectively 1-1 (injection / monomorphism / section) from X to Y, since one can (almost) get back to x with the other half of the pair;
2. ap.from:(Y=>X) applied to ap.to(x) may not get back to x, but it will get back to something that is compatible with x, so that they could be combined. In the common case where X is Distinguishable it does get back to x. Conversely ap.from will fail (Fail.next) if its parameter does not come from an X, except that if X is a procedure type it might instead return a procedure that fails when called.

The most obvious place where AdjointPair is used is in an isA declaration. Now if X isA Y via apxy, and P isA Q via appq, then there is an induced relation:

Y=>P isA X=>Q via AdjointPair(
   { `yp = $=:Y=>P; { appq.to (yp (apxy.to $)) }} : (Y=>P)=>(X=>Q)},
   { `xq = $=:X=>Q; { appq.from (xq (apxy.from $)) }} : (X=>Q)=>(Y=>P)})

The 2nd (.from) procedure doesn’t itself fail, but instead it returns a procedure that might fail if given a Y that isn’t an X. The key point is that if you start with a Y=>P, convert to an X=>Q, then convert back, then you get back to a procedure that has the same semantics, just some extra unnecessary checks thrown in. One might well say that this transformation is a natural one. Maybe if we define an appropriate category then these really are an adjoint pair in the Category Theory sense. Anybody who can see that and explain it will get a permanent acknowledgement in Wombat’s main documentation. For extra merit: What then is the associated monad?

Adventures in combining procedures

Gaussian Integers are just complex numbers with integer real and imaginary parts. Why don't they just call them Complex Integers? That's what I'll do here.

Suppose we have types Int, Rational and ComplexInteger, such that Int isA Rational and Int isA ComplexInteger.

Imagine a procedure that takes a Union(Rational,ComplexInteger). Any well behaved such procedure is going to give the same result for an Int parameter, whether it arrives as a Rational (with denominator 1) or as a ComplexInteger (with imaginary part 0). Indeed by transitivity, Int isA Union(Rational,ComplexInteger), so it can just come as itself. For definiteness let's suppose the procedure returns the magnitude as an AlgebraicNumber. The traditional hacky approach is to use the equivalent of Wombat's firstCase:

  `magnitude =
    { firstCase $ of [
        { $=`p:ComplexInteger; AlgebraicNumber.sqrt(p.real**2 + p.imag**2) }
        { $=`p:Rational; AlgebraicNumber.abs(p) }
    ]}

Int parameter's will always take the first exit (even if Rational!). The more respectable way to code this is to use the case operator:

  `magnitude =
    { case $ of [
        { `p = $=:ComplexInteger; AlgebraicNumber.sqrt(p.real**2 + p.imag**2) }
        { `p = $=:Rational; AlgebraicNumber.abs(p) }
    ]}

Note that the procedures are still given as a list here, but are actually a set in this instance (with no order), or rather a SemiSet, but we can use list operator because List X convertsTo SemiSet X.

In this 2nd implementation using case, when magnitude is given an Int parameter it will (in theory) run both procedures to conclusion and check that they return the same result. However a runtime check might not be necessary if the compiler can work out that both return the same answer, and in that  case it can choose the more efficient.

The case operator is precisely the mechanism for combining procedures. So we can imagine a class of generic procedures such that, if the procedure is defined for types X and Y, then it is also automatically defined for Union(X,Y). Wombat supports such generic procedures via properties of types. In this case it is natural to make .magnitude a method by making it a case in the type's .asProc static property. This is convenient, allowing one to write expr.magnitude. Other static properties of types can be used for generic procedures that don't fit the .asProc pattern. Except that Wombat doesn't do duck-typing. So the automatic combination of .asProc and other properties only applies where both types get the property from the same Behaviour, but we'll gloss over that for the moment.

Let's see if we can prove in an informal way that this works correctly. Suppose we have, as well we might, a type ComplexRational such that there are declared relations: Rational isA ComplexRational and ComplexInteger isA ComplexRational. The rules say that Union(Rational,ComplexInteger) isA ComplexRational. Suppose (simplifying) that the .magnitude operation for the Union is formed by combining the operations for Rational and ComplexInteger. We know that the .magnitude operation for Rational is compatible with that for ComplexRational, and ditto for ComplexInteger. Now consider the operation of .magnitude on a Union value. If the Rational branch fails then the ComplexInteger branch is the one that wins, and it is compatible with the result for ComplexRational. Conversely if the ComplexInteger case fails the Rational branch result will be compatible. If both succeed then the two results are compatible with each other, and each is separately compatible with the .magnitude of ComplexRational. The combination then has to be compatible as well. Hopefully I can make a less hand-wavy proof one day.

I was going to continue with a discussion of folds. For associative operations, foldl and foldr can be combined (and maybe we can add other potentially parallel variants), and one can imagine adding a little magic pixie-dust that will allow the compiler to pick the best for various available implementations of List. However that will have to wait for another day.