Behaviours, Bases, Modes and Properties

Behaviours, Bases, Modes and Properties

[This is just a copy from this docs file: https://docs.google.com/document/d/1wJoLRP9bV70d7bL_JNF2pk7U0cvHQ1lNevDOI09FDG8/edit?usp=sharing. I finally found a reasonable way to move docs to blogger: export as html, open that and copy-paste into blogger.]

[I plan to change the name from Wombat, perhaps to Emmy, in honour of Emmy Noether]

The term "Type" is overloaded, with some saying the values can only have one type, but others allowing subtyping, so that values of a subtype are also of the higher type. To avoid this confusion, and also because both concepts are needed, Wombat has two separate notions:

• 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

All values have a unique Base. Programmers usually deal with modes rather than bases, since they support subtyping (submoding).

There are primitive Bases which come from the compilation target. For example if the target is Amd64, then Int64 (the type of 64 bit Integers) might be a primitive Base with properties derived from the hardware manual.

All other Bases have one or more implementations. The implementations need not be primitive, but there can only be a finite chain of implementedBy before getting to primitive Bases. At run time all values are of a primitive Base.

Bases are characterised by properties (which come bundled in Behaviours). Access to values is only through the properties of its Base: peeking at the implementation is only allowed in a controlled way to optimize. The properties of a Base are implemented using the properties of the implementing Base.

Bases are organized in a partial order by the isA relationship (which derives from the reflexive and transitive closure of all isA declarations). For example we might have Integer isA Rational. This definition provides an inverse pair of procedures between the two Bases (the up procedure is total, and the procedures are inverses).

When two Bases are linked by an isA relationship then any properties they both have must be compatible. This means that the values must be combinable, as explained in a later section. A Base inherits properties that it doesn't already have, so that, for example, Integer will inherit the denominator property from Rational.

There can be indexed families of Bases. For example List is indexed by Base, so for any base X, List X is another Base.

Necessary rule: all chains (totally ordered subsets) of Bases must be finite, so they have a maximum and minimum element. For example we couldn't have: forall X: X isA List X, because that would create an infinite chain with no maximal element.

We also have the rule that a base can only have a finite number of bases above it and below it in the hierarchy. This is necessary to make combine work -- see below.

Properties and Behaviours

Values known at compile time can have properties, which are simply named values.

Properties are always defined in a bundle, called a Behaviour. A Behaviour specifies what Base of value it can apply to. For example the monad behaviour can apply to a base=>base. We are mostly concerned with the properties of Bases, and how that translates to the properties of Modes.

[Of course the isA PO on base induces a PO on base=>base, but I don't know how all this can be generalized to such induced POs.]

A property is characterised by (a) the Behaviour it comes from; (b) the name (an Atom); (c) the how index (since a value can conform to a Behaviour in more than one way). The same property can apply to multiple Bases in the Base hierarchy, but when it does it is required to be consistent when one is above the other in the hierarchy. For example the ".add" property is required to be compatible between Integer and Rational. [Well actually it is the .binop property from behaviour CommutativeGroup with how index .add.]

Behaviours are also organized in a hierarchy that is a lattice by extends.

Modes

Modes are based on Bases, but add subtyping (which might be called submoding, but I won't). We create the Modes as follows:

• 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]).

Values belong to multiple Modes. If a value, v, has a particular Base, B, then it belongs to the corresponding Mode, and also every Mode above it in the Mode lattice.

Modes have properties derived from those of Bases. Every property of a Base extends to the corresponding Mode, and also to every Mode below that which doesn't already have that property (if it does have the property then it is required to be compatible).

Compatibility (combine operation)

Firstly we note that if a procedure isn't surjective/onto, then for many purposes the output type might as well be Any. And for partial functions, which may fail for some values of the specified input type, then for many purposes the input type might as well be Any. While this is arguable, it does make it easier to talk about the following, and we will only be considering partial procedure types of type Any=>Any.

Distinguishable is a Behaviour, and Bases that conform to it support equality (= op for our purposes). A weaker behaviour is Combinable which defines the combine operation. For types that support equality, combine checks that the values are equal, and returns that value if so (otherwise failing). The most important Base that doesn't conform to Distinguishable is procedures. But they also support combine is the following way:

• 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

We'll consider the Behaviour Add with property .add, defined thus (approximately, leaving out "how"):

`Add = newBehaviour Base {$=`B:Base; `M=B:Mode; struct [
                                                .add->(M*M)=>M
                                              ]}; ...

Integer conformsTo Add by { struct [ .add->integerAdd ] };

Rational conformsTo Add by { struct [ .add->rationalAdd ] };

Integer isA Rational by (integerToRational,rationalToInteger);

Integer can't inherit .add from Rational, because it already has it. What happens, to prove compatibility, is that the two .add procedures get combined into one. Here's how that works:

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

Now suppose that we have a Base ComplexInt (i.e. Gaussian integer), with .add defined, but that Integer itself does not have .add defined:

ComplexInt conformsTo Add by { struct [ .add->complexIntAdd ] };

Rational conformsTo Add by { struct [ .add->rationalAdd ] };

Integer isA Rational by (integerToRational,rationalToInteger);

Integer isA ComplexInt by (integerToGaussian,gaussianToInteger);

Now Integer inherits different .add from both parents. Once again the solution is that the .add properties are combined. So when two integers are added then: (a) we convert them to rational and add that; (2) we convert them to complex and add that. To check equality we have to force the two results to the intersection (which is Integer) and check equality there. Which succeeds!

Obviously these combined operations are likely to be inefficient. It is expected that all important cases can be optimized, but not necessarily automatically.

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.