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?