Ko

A language for programming recursive circuits

Ko
2. Language
2.2. Type system
2.2.1. Type unification
2.2.1. Type unification

Type “unification” is an operation that the compiler performs in all places of a Ko program where: (i) multiple values are combined into a sequence, or (ii) different code paths return values at the same place (e.g. the Yield macro macro).

Unification for sequences

In the first case, type unification helps determine a type for the resulting sequence, while allowing safe variation in the types of the comprising values. For instace, the following function tries to create a sequence out of a String element and a (String) (sequence of strings) element.

MakeSeqSeqString() {   // returns type ((String))
	return: (
		"abc"    // type String
		("def", "ghi")   // type (String)
	)
}

Unification will find the smallest type such that both elements, String and (String) , are assignable to. Thus the unified element type is derived to be (String) . As a result, the function will return a sequence of sequence of strings, i.e. ((String)) .

Unification for branching

In the second case, unification ensures that regardless of which of two code paths deliver a value to the same location, that value's type can be known before execution unambiguously. This scenario is embodied in the Yield macro. For instance,

SaySomething(casual) {   // casual is a boolean argument
	return: Yield(
		if: casual
		then: "hi"
		else: ("hello", "world")
	)
}

In this example, which of the two values ( "hi" or ("hello", "world") ) is returned is something that can only be determined at runtime, after the value of the boolean casual is known.

However, the smallest common type that accommodates both values can be determined at compile time, and it is (String) , as in the previous example. Knowing the type of branching operations before they have happened is one of the key reasons for Ko's compiler ability do complete type inference.

The algebra of unification

Let U denote the binary (two-argument) operation of type unification, and let p , q and r be types. Unification is both commutative, U(p, q) = U(q, p) , and associative, U(p, U(q, r)) = U(U(p, q), r) .

To define unification we use the Empty type to denote places where no value was passed to a function argument in the Ko program (this is determined at compile-time).

Unification greedily follows the recursive rules:

U(P, Empty) = *P
U(P,(Q)) = (U(P,Q))   // for type T, (T) means "sequence of T" 
U(*P, (Q)) = (U(P, Q))

When two structure types p and q are being unified, U(p, q) , the result is a new structure. The unified structure has fields unifying the corresponding (by name) fields in p and q . If either p or q has a field which is missing in its counterpart, then this field is assumed present (in the counterpart structure) with type Empty .