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 =

{ c

**ase**$

**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

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

**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.

## No comments:

## Post a Comment