The Lattice of Kinds

Home
Services
kinds
Chapter 2: Kinds
The Lattice of Kinds

Placing a partial order on kinds according to whether one conforms to another.

§1. Conformance. If we write \(K\leq L\) to mean that \(K\) conforms to \(L\), then \(\leq\) provides an ordering on kinds. For any kinds \(K, L, M\) not making use of kind variables¹ it is true that:

● \(K \leq K\) — reflexivity.
● If \(K\leq L\) and \(L\leq M\) then \(K\leq M\) — transitivity.
● K_nil \(\leq K \leq\) value — there are top and bottom elements.²
● If \(K \leq L\) then a value of kind \(K\) can always be substituted for a value of kind \(L\) without modification — the Liskov substitution principle.³
● There is a join \(K\lor L\) and a meet \(K\land L\) such that \(K\land L\leq K, L\leq K\lor L\), where \(K\lor L\) is minimal and \(K\land L\) maximal with that property.

¹ Introducing kind variables complicates the picture, because whether or not list of K conforms to list of arithmetic values depends on the current value of K and therefore on the current context. ↩
² K_nil is a kind which exists only for kind-checking purposes, meaning "a member of the empty set". Clearly no value can ever have this. This differs from K_void, which means "the absence of a value". Neither can ever be the kind of a variable, of course. ↩
³ Also known as strong behavioural subtyping. This only applies to definite kinds, because no value ever has an indefinite kind. ↩

§2. In general there is no guarantee of antisymmetry, i.e., that \(K\leq L\) and \(L\leq K\) must mean \(K = L\), nor that \(K\lor L\) or \(K\land L\) are unique. We could imagine creating indefinite kinds rhyming with lumber value and calculator value such that number and real number would conform to both. If so, then either one of rhyming with lumber value and calculator value could equally well serve as \(K\lor L\). The set of kinds is therefore not formally a lattice.

As it happens, however, Inform's choice of indefinite kinds is made in such a way that this does not happen. The upshot is that although the set of kinds is not necessarily a lattice, it often will be in practice, and we use the language of lattices — hence, words like "join" and "meet" — as a guide.

§3. Conformance is tested with the function Kinds::conforms_to, and the following shows it in action.

'new kind thing of object': ok
'new kind device of thing': ok
'new kind vehicle of thing': ok
'new unit length': ok
'number <= number?': true
'number <= real number?': false
'value <= number?': false
'object <= text?': false
'object <= thing?': false
'thing <= object?': true
'device <= thing?': true
'device <= object?': true
'list of devices <= thing?': false
'list of devices <= list of things?': true

§4. The indefinite arithmetic kind used by Inform is a good example of what in other languages would be called a protocol. Here we see conformance:

'new unit length': ok
'number <= arithmetic value?': true
'real number <= arithmetic value?': true
'length <= arithmetic value?': true
'text <= arithmetic value?': false
'arithmetic value <= value?': true
'value <= arithmetic value?': false
'arithmetic value <= sayable value?': true

§5. Here we see covariance versus contravariance:

'new kind larger of object': ok
'new kind smaller of larger': ok
'smaller <= larger?': true
'larger <= smaller?': false
'list of smaller <= list of larger?': true
'list of larger <= list of smaller?': false
'relation of larger to texts <= relation of smaller to texts?': false
'relation of smaller to texts <= relation of larger to texts?': true
'phrase larger -> text <= phrase smaller -> text?': true
'phrase smaller -> text <= phrase larger -> text?': false
'phrase text -> larger <= phrase text -> smaller?': false
'phrase text -> smaller <= phrase text -> larger?': true

● A constructor \(\phi\) is "covariant" — meaning, goes the same way — if \(K\leq L\) means \(\phi(K)\leq\phi(L)\).
● It is "contravariant" — goes the opposite way — if \(K\leq L\) means \(\phi(L)\leq\phi(K)\).

Note that "list of ..." is covariant; "phrase ... -> ..." is contravariant in the first term, but covariant in the second. To see why, consider a function \(f: K\to L\), and then considering expanding or contracting the sets \(K\) and \(L\). It's no problem if \(L\) grows larger — \(f\) can still be used — but if \(L\) shrinks then \(f\) might map outside it, which is unsafe. But the reverse is true for \(K\). If \(K\) shrinks we can still use \(f\), but if it grows then we may not be able to. If \(K_1\leq K\leq K_2\) and \(L_1\leq L\leq L_2\), then a function \(f:K\to L\) is also a function \(K_1\to L_2\), but not \(K_2\to L_1\).

See Latticework::order_relation for more.

define COVARIANT 1
define CONTRAVARIANT -1

§6. Lattice operations. Every \(K\) other than value, K_nil and K_void has a minimal element \(K^+\) such that \(K\leq K^+\) but \(K\neq K^+\): we call this the "superkind" of \(K\). Assuming kinds form a lattice, this will be unique. The following function returns the superkind, or NULL for special cases which do not have one.

It is in this function that the basic conformance facts are expressed. We hard-code that for the built-in indefinite kinds, and give the client tool a chance to provide other conformances. For Inform, for example, the callback function is what tells us that the superkind of man is person.

kind *Latticework::super(kind *K) {
    if (Kinds::eq(K, K_real_arithmetic_value)) return K_arithmetic_value;
    if (Kinds::eq(K, K_enumerated_value)) return K_understandable_value;
    if (Kinds::eq(K, K_arithmetic_value)) return K_understandable_value;
    if (Kinds::eq(K, K_understandable_value)) return K_sayable_value;
    if (Kinds::eq(K, K_pointer_value)) return K_sayable_value;
    if (Kinds::eq(K, K_sayable_value)) return K_stored_value;
    if (Kinds::eq(K, K_stored_value)) return K_value;
    if (Kinds::eq(K, K_value)) return NULL;
    if (Kinds::eq(K, K_nil)) return NULL;
    if (Kinds::eq(K, K_void)) return NULL;
    #ifdef HIERARCHY_GET_SUPER_KINDS_CALLBACK
    kind *S = HIERARCHY_GET_SUPER_KINDS_CALLBACK(K);
    if (S) return S;
    #endif
    if (KindConstructors::compatible(K->construct, K_real_arithmetic_value->construct, FALSE))
        return K_real_arithmetic_value;
    if (KindConstructors::compatible(K->construct, K_enumerated_value->construct, FALSE))
        return K_enumerated_value;
    if (KindConstructors::compatible(K->construct, K_arithmetic_value->construct, FALSE))
        return K_arithmetic_value;
    if (KindConstructors::compatible(K->construct, K_pointer_value->construct, FALSE))
        return K_pointer_value;
    if (KindConstructors::compatible(K->construct, K_understandable_value->construct, FALSE))
        return K_understandable_value;
    if (KindConstructors::compatible(K->construct, K_sayable_value->construct, FALSE))
        return K_sayable_value;
    if (KindConstructors::compatible(K->construct, K_stored_value->construct, FALSE))
        return K_stored_value;
    return K_value;
}

§7. Joins are defined above. So are meets, though in practice they are never useful to us except as a way of calculating joins: the two are dual to each other as they pass through contravariant constructors.

The main use of this for Inform is to handle literals such as:

{ 1, 2.1415, "frog" }

The kind of this is by definition the join of the kinds of the values in the list, which as it happens is K_sayable_value — an indefinite kind, so that such a list can't be constructed as data.

kind *Latticework::join(kind *K1, kind *K2) {
    return Latticework::j_or_m(K1, K2, 1);
}

kind *Latticework::meet(kind *K1, kind *K2) {
    return Latticework::j_or_m(K1, K2, -1);
}

kind *Latticework::j_or_m(kind *K1, kind *K2, int direction) {
    if (K1 == NULL) return K2;
    if (K2 == NULL) return K1;
    kind_constructor *con = K1->construct;
    int a1 = KindConstructors::arity(con);
    int a2 = KindConstructors::arity(K2->construct);
    if ((a1 > 0) || (a2 > 0)) {
        if (K2->construct != con) return K_value;
        kind *ka[MAX_KIND_CONSTRUCTION_ARITY] = { NULL, };
        for (int i=0; i<a1; i++)
            if (con->variance[i] == COVARIANT)
                ka[i] = Latticework::j_or_m(K1->kc_args[i], K2->kc_args[i], direction);
            else
                ka[i] = Latticework::j_or_m(K1->kc_args[i], K2->kc_args[i], -direction);
        if (a1 == 1) return Kinds::unary_con(con, ka[0]);
        else return Kinds::binary_con(con, ka[0], ka[1]);
    } else {
        Deal with nil7.1;
        Deal with floating-point promotions7.2;
        if (Kinds::conforms_to(K1, K2)) return (direction > 0)?K2:K1;
        if (Kinds::conforms_to(K2, K1)) return (direction > 0)?K1:K2;
        if (direction > 0) {
            for (kind *K = K1; K; K = Latticework::super(K))
                if (Kinds::conforms_to(K2, K))
                    return K;
            return K_value;
        } else {
            return K_nil;
        }
    }
}

§7.1. This ensures that \(K\land\) K_nil \( = \) K_nil, and that \(K\lor\) K_nil \( = K\).

Deal with nil7.1 =

    if ((Kinds::eq(K1, K_nil))) return (direction > 0)?K2:K1;
    if ((Kinds::eq(K2, K_nil))) return (direction > 0)?K1:K2;

This code is used in §7.

§7.2. If one of \(K_1\), \(K_2\) uses floating-point and the other doesn't, then we promote the one which doesn't before taking the join. This is useful when inferring the kind of a constant list or column which mixes floating-point and integer literals; recall that number \(\not\leq\) real number, so without this promotion there would be no way to join such kinds.

Deal with floating-point promotions7.2 =

    if ((Kinds::FloatingPoint::uses_floating_point(K1) == FALSE) &&
        (Kinds::FloatingPoint::uses_floating_point(K2)) &&
        (Kinds::eq(Kinds::FloatingPoint::real_equivalent(K1), K2)))
        return (direction > 0)?K2:K1;
    if ((Kinds::FloatingPoint::uses_floating_point(K2) == FALSE) &&
        (Kinds::FloatingPoint::uses_floating_point(K1)) &&
        (Kinds::eq(Kinds::FloatingPoint::real_equivalent(K2), K1)))
        return (direction > 0)?K1:K2;

This code is used in §7.

§8. Compatibility. A related but different question is "compatibility". This asks whether a value of kind \(K\) can be used where \(L\) is expected, but:

(i) It is now okay if explicit code to perform a conversion would be needed; and
(ii) There are now three possible answers — always, never and sometimes, where "sometimes" means that code can be compiled which would test compatibility at run time rather than compile time.

Conformance implies compatibility but not vice versa. For example:

'new kind thing of object': ok
'new kind device of thing': ok
'new kind vehicle of thing': ok
'new unit length': ok
'number compatible with number?': always
'number compatible with real number?': always
'value compatible with number?': never
'object compatible with text?': never
'object compatible with thing?': sometimes
'thing compatible with object?': always
'device compatible with thing?': always
'device compatible with object?': always
'list of devices compatible with thing?': never
'list of devices compatible with list of things?': always
'relation of things to texts compatible with relation of devices to texts?': never
'relation of devices to texts compatible with relation of things to texts?': always
'phrase thing -> text compatible with phrase device -> text?': always
'phrase device -> text compatible with phrase thing -> text?': never
'phrase text -> thing compatible with phrase text -> device?': never
'phrase text -> device compatible with phrase text -> thing?': always
'activity on numbers compatible with activity?': always
'first term of activity': nothing
'activity on numbers compatible with activity on values?': never

Note that number is compatible with real number. Run-time code will be needed to convert the value, but the answer is "always". We also see that device is always compatible with thing — every device is a thing — but also that thing is sometimes compatible with device. If we pass a thing to a function expecting to see a device, run-time code can check whether the value passed is indeed a device, and reject the call with a run-time error if not.

§9. Kind checking can happen for many reasons, but the most difficult case occurs when matching phrase prototypes. This is difficult because it involves kind variables:

To add (new entry - K) to (L - list of values of kind K) ...

This matches "add 23 to U" if "L" is a list of numbers, but not if it is a list of times.

Since kind variables can be changed only when matching phrase prototypes, and this is not a recursive process, we can store the current definitions of A to Z in a single array.

define MAX_KIND_VARIABLES 27  we number them from 1 (A) to 26 (Z)

kind *values_of_kind_variables[MAX_KIND_VARIABLES];

§10. In theory the kind-checker only needs to read the values of A to Z, not to write them. If Q is currently equal to number, then it should check kinds against Q exactly as if it were checking against number. It can indeed do this — that's the MATCH_KIND_VARIABLES_AS_VALUES mode. It can also ignore the values of kind variables and treat them as names, so that Q matches only against Q, regardless of its current value; that's the MATCH_KIND_VARIABLES_AS_SYMBOLS mode. Or it can match anything against Q, which is MATCH_KIND_VARIABLES_AS_UNIVERSAL mode.

More interestingly, the kind-checker can also set the values of A to Z. This is convenient since checking their correctness is more or less the same thing as inferring what they seem to be in a given situation. So this is MATCH_KIND_VARIABLES_INFERRING_VALUES mode.

define MATCH_KIND_VARIABLES_AS_SYMBOLS 0
define MATCH_KIND_VARIABLES_INFERRING_VALUES 1
define MATCH_KIND_VARIABLES_AS_VALUES 2
define MATCH_KIND_VARIABLES_AS_UNIVERSAL 3

int kind_checker_mode = MATCH_KIND_VARIABLES_AS_SYMBOLS;

§11. When the kind-checker does choose a value for a variable, it not only sets the relevant entry in the above array but also creates a note that this has been done. (If a phrase is correctly matched by the specification matcher, a linked list of these notes is attached to the results: thus a match of "add 23 to U" in the example above would produce a successful result plus a note that K has to be list of numbers.)

typedef struct kind_variable_declaration {
    int kv_number;  must be from 1 to 26
    struct kind *kv_value;  must be a definite non-NULL kind
    struct kind_variable_declaration *next;
    CLASS_DEFINITION
} kind_variable_declaration;

The structure kind_variable_declaration is accessed in 3/dmn and here.

§12. And this little function unpacks a list of KVDs into an array of values:

void Latticework::unpack_kvd(kind **vals, kind_variable_declaration *kvd) {
    for (int i=0; i<27; i++) vals[i] = NULL;
    for (; kvd; kvd=kvd->next) vals[kvd->kv_number] = kvd->kv_value;
}

§13. Common code. So the following routine tests conformance if comp is FALSE, returning ALWAYS_MATCH if and only if from \(\leq\) to holds; and otherwise it tests compatibility, returning ALWAYS_MATCH, SOMETIMES_MATCH or NEVER_MATCH as appropriate.

int Latticework::order_relation(kind *from, kind *to, int allow_casts) {
    if (Kinds::get_variable_number(to) > 0) {
        kind *var_k = to, *other_k = from;
        Deal separately with matches against kind variables13.7;
    }
    if (Kinds::get_variable_number(from) > 0) {
        kind *var_k = from, *other_k = to;
        Deal separately with matches against kind variables13.7;
    }
    Deal separately with the sayability of lists13.1;
    Deal separately with the top and bottom of the lattice13.2;
    Deal separately with the special role of the unknown kind13.3;
    The general case of compatibility13.4;
}

§13.1. A list is sayable if and only if it is empty, or its contents are sayable.

Deal separately with the sayability of lists13.1 =

    if ((Kinds::get_construct(from) == CON_list_of) &&
        (Kinds::eq(to, K_sayable_value))) {
        kind *CK = Kinds::unary_construction_material(from);
        if (Kinds::eq(CK, K_nil)) return ALWAYS_MATCH;
        if (CK == NULL) return ALWAYS_MATCH;  for an internal test case making dodgy lists
        return Latticework::order_relation(CK, K_sayable_value, allow_casts);
    }

This code is used in §13.

§13.2. Deal separately with the top and bottom of the lattice13.2 =

    if (Kinds::eq(to, K_value)) return ALWAYS_MATCH;
    if (Kinds::eq(from, K_nil)) return ALWAYS_MATCH;

This code is used in §13.

§13.3. NULL as a kind means "unknown". It's compatible only with itself and, of course, "value".

Deal separately with the special role of the unknown kind13.3 =

    if ((to == NULL) && (from == NULL)) return ALWAYS_MATCH;
    if ((to == NULL) || (from == NULL)) return NEVER_MATCH;

This code is used in §13.

§13.4. The general case of compatibility13.4 =

    int f_a = KindConstructors::arity(from->construct);
    int t_a = KindConstructors::arity(to->construct);
    int arity = (f_a < t_a)?f_a:t_a;
    int o = ALWAYS_MATCH;
    if (from->construct != to->construct)
        o = Latticework::construct_compatible(from, to, allow_casts);
    int i, this_o = NEVER_MATCH, fallen = FALSE;
    for (i=0; i<arity; i++) {
        if ((Latticework::vacuous(from->kc_args[i])) && (Latticework::vacuous(to->kc_args[i])))
            continue;
        if (KindConstructors::variance(from->construct, i) == COVARIANT)
            this_o = Latticework::order_relation(from->kc_args[i], to->kc_args[i], allow_casts);
        else {
            this_o = Latticework::order_relation(to->kc_args[i], from->kc_args[i], allow_casts);
        }
        switch (this_o) {
            case NEVER_MATCH: o = this_o; break;
            case SOMETIMES_MATCH: if (o != NEVER_MATCH) { o = this_o; fallen = TRUE; } break;
        }
    }
    if ((fallen) && (to->construct != CON_list_of)) return NEVER_MATCH;
    return o;

This code is used in §13.

§13.5.

int Latticework::vacuous(kind *K) {
    if ((Kinds::eq(K, K_nil)) || (Kinds::eq(K, K_void))) return TRUE;
    return FALSE;
}

§13.6.

int Latticework::construct_compatible(kind *from, kind *to, int allow_casts) {
    kind *K = from;
    while (K) {
        if (Kinds::eq(K, to)) return ALWAYS_MATCH;
        K = Latticework::super(K);
    }
    if ((allow_casts) && (KindConstructors::find_cast(from->construct, to->construct)))
        return ALWAYS_MATCH;
    K = to;
    while (K) {
        if (Kinds::eq(K, from)) {
            #ifdef HIERARCHY_ALLOWS_SOMETIMES_MATCH_KINDS_CALLBACK
            if (HIERARCHY_ALLOWS_SOMETIMES_MATCH_KINDS_CALLBACK(from))
                return SOMETIMES_MATCH;
            #endif
            #ifndef HIERARCHY_ALLOWS_SOMETIMES_MATCH_KINDS_CALLBACK
            return SOMETIMES_MATCH;
            #endif
        }
        K = Latticework::super(K);
    }
    return NEVER_MATCH;
}

§13.7. Recall that kind variables are identified by a number in the range 1 ("A") to 26 ("Z"), and that it is also possible to assign them a domain, or a "declaration". This marks that they are free to take on a value, within that domain. For example, in

To add (new entry - K) to (L - list of values of kind K) ...

the first appearance of K will be an ordinary use of a kind variable, whereas the second has the declaration value — meaning that it can become any kind matching value. (It could alternatively have had a more restrictive declaration like arithmetic value.)

Deal separately with matches against kind variables13.7 =

    switch(kind_checker_mode) {
        case MATCH_KIND_VARIABLES_AS_SYMBOLS:
            if (Kinds::get_variable_number(other_k) ==
                Kinds::get_variable_number(var_k)) return ALWAYS_MATCH;
            return NEVER_MATCH;
        case MATCH_KIND_VARIABLES_AS_UNIVERSAL: return ALWAYS_MATCH;
        default: {
            int vn = Kinds::get_variable_number(var_k);
            if (Kinds::get_variable_stipulation(var_k))
                Act on a declaration usage, where inference is allowed13.7.1
            else
                Act on an ordinary usage, where inference is not allowed13.7.2;
        }
    }

This code is used in §13 (twice).

§13.7.1. When the specification matcher works on matching text such as

add 23 to the scores list;

it works through the prototype:

To add (new entry - K) to (L - list of values of kind K) ...

in two passes. On the first pass, it tries to match the tokens "23" and "scores list" against K and list of values of kind K respectively in MATCH_KIND_VARIABLES_INFERRING_VALUES mode; on the second pass, it does the same in MATCH_KIND_VARIABLES_AS_VALUES mode. In this example, on the first pass we infer (from the kind of "scores list", which is indeed a list of numbers) that K must be number; on the second pass we verify that "23" is a K.

The following shows what happens matching values of kind K, which is a declaration usage of the variable K.

Act on a declaration usage, where inference is allowed13.7.1 =

    switch(kind_checker_mode) {
        case MATCH_KIND_VARIABLES_INFERRING_VALUES:
            if (Latticework::order_relation(other_k,
                Kinds::get_variable_stipulation(var_k), allow_casts) != ALWAYS_MATCH)
                return NEVER_MATCH;
            LOGIF(KIND_CHECKING, "Inferring kind variable %d from %u (declaration %u)\n",
                vn, other_k, Kinds::get_variable_stipulation(var_k));
            values_of_kind_variables[vn] = other_k;
            kind_variable_declaration *kvd = CREATE(kind_variable_declaration);
            kvd->kv_number = vn;
            kvd->kv_value = other_k;
            kvd->next = NULL;
            return ALWAYS_MATCH;
        case MATCH_KIND_VARIABLES_AS_VALUES: return ALWAYS_MATCH;
    }

This code is used in §13.7.

§13.7.2. Whereas this is what happens when matching just K. On the inference pass, we always make a match, which is legitimate because we know we are going to make a value-checking pass later.

Act on an ordinary usage, where inference is not allowed13.7.2 =

    switch(kind_checker_mode) {
        case MATCH_KIND_VARIABLES_INFERRING_VALUES: return ALWAYS_MATCH;
        case MATCH_KIND_VARIABLES_AS_VALUES:
            LOGIF(KIND_CHECKING, "Checking %u against kind variable %d (=%u)\n",
                other_k, vn, values_of_kind_variables[vn]);
            if (Latticework::order_relation(other_k,
                values_of_kind_variables[vn], allow_casts) == NEVER_MATCH)
                return NEVER_MATCH;
            else
                return ALWAYS_MATCH;
    }

This code is used in §13.7.

§14. It's easy to confused when writing a type checker, especially with variables getting in the way, so these logging functions can be helpful:

void Latticework::show_variables(void) {
    LOG("Variables: ");
    for (int i=1; i<=26; i++) {
        kind *K = values_of_kind_variables[i];
        if (K == NULL) continue;
        LOG("%c=%u ", 'A'+i-1, K);
    }
    LOG("\n");
}

void Latticework::show_frame_variables(void) {
    int shown = 0;
    for (int i=1; i<=26; i++) {
        kind *K = Kinds::variable_from_context(i);
        if (K) {
            if (shown++ == 0) LOGIF(MATCHING, "Stack frame uses kind variables: ");
            LOGIF(MATCHING, "%c=%u ", 'A'+i-1, K);
        }
    }
    if (shown == 0) LOGIF(MATCHING, "Stack frame sets no kind variables");
    LOGIF(MATCHING, "\n");
}