An overview of the kinds module's role and abilities.

§1. Prerequisites. The kinds module is a part of the Inform compiler toolset. It is presented as a literate program or "web". Before diving in:

§2. Kinds, definiteness, and safety. To begin, an overview of the type system used by Inform, since this module is essentially an isolated implementation of it.

Inform is like most programming languages in that it deals with a rich variety of values, that is, individual pieces of data. The number 17, the time "3:15 PM" and the "Entire Game" (a named scene) are all examples of values. Except that Inform uses the word "kind" rather than "type" for the different sorts of values which exist, I have tried to follow conventional computer-science terminology in this source code.1

Kinds such as number are "definite", in that they unambiguously say what format a piece of data has. If the compiler can prove that a value has a definite kind, it knows exactly how to print it, initialise it and so on. Variables, constants, literal values and properties all have definite kinds.

But other kinds, such as arithmetic value, merely express a guarantee that a value can be used in some way. These are "indefinite". In some contemporary languages this latter meaning would be a "typeclass" (e.g., Haskell) or "protocol" (e.g., Swift) but not a "type".2 The ultimate in indefiniteness is the kind value, which expresses only that something is a piece of data. Phrase tokens can be indefinite, as this example shows:

To display (X - an arithmetic value):

§3. The virtue of knowing that a piece of data has a given kind is that one can guarantee that it can safely be used in some way. For example, it is unsafe to divide by a text, and an attempt to do so would be meaningless at best, and liable to crash the compiled program at worst. The compiler must therefore reject any requests to do so. That can only be done by constant monitoring of their kinds of all values being dealt with.

Inform is a high-level language designed for ease of use. Accordingly:

§4. One caveat: Inform provides low-level features allowing Inter code to be injected directly into the compiler's output, bypassing all kind checking. For instance:

To decide which text is (N - a number) as text: (- {N} -).

is analogous to a C function like so: 

    char *number_as_text(int N) {
        return (char *) N;
    }

This is a legal C function but the deliberate disregard of type safety — in the use of the (char *) cast notation — is a kind of waiver, where the author chooses to accept the risk. In a similar way, there are no victims of Inform's (- and -) notation, only volunteers.

§5. Kinds and knowledge. Inform uses the kinds system when building its world model of knowledge, and not only to monitor specific computational operations. For example, if the source text says:

A wheelbarrow is a kind of vehicle. The blue garden barrow is a wheelbarrow.

then the value "blue garden barrow" has kind wheelbarrow, which is within vehicle, within thing, within object. As this example suggests, knowledge and property ownership passes through a single-inheritance hierarchy; that is, each kind inherits directly from only one other kind.

§6. A strongly typed language mixing static and dynamic typing. Programming languages with types are often classified by two criteria. One is how rigorously they maintain safety, with safer languages being strongly typed, and more libertarian ones weakly typed. The other is when types are checked, with statically typed languages being checked at compile time, dynamically typed languages being checked at run-time. Both strong/weak and static/dynamic are really ranges of possibilities.

§7. Dimensional analysis. Inform subjects all calculations with its "quasinumerical" kinds — basically, all those on which calculation can be performed — to dimensional checking.

Dimension in this sense is a term drawn from physics. The idea is that when quantities are multiplied together, their natures are combined as well as the actual numbers involved. For instance, in $$ v = f\lambda $$ if the frequency \(f\) of a wave is measured in Hz (counts per second), and the wavelength \(\lambda\) in m, then the velocity \(v\) must be measured in m/s: and that is indeed a measure of velocity, so this looks right. We can tell that the formula $$ v = f^2\lambda $$ must be wrong because it would result in an acceleration. Physicists use the term "dimensions" much as computer-scientists use the word "type", and Inform follows suit.

See Dimensions for a much fuller discussion.

§8. Conformance and compatibility. One kind \(K\) "conforms to" another kind \(L\) if values of \(K\) can always be used where values of \(L\) are expected. For example, in a typical work of IF produced by Inform, the kind vehicle conforms to thing. This idea can also apply to kinds of kinds: number conforms to arithmetic value which conforms to sayable value, for example. See The Lattice of Kinds for how conformance produces a hierarchical order among possible kinds.

Conformance is an "is-a" relationship: thus a vehicle can safely be stored in a variable of kind thing because a vehicle is a thing. But a number cannot be stored in a real number variable directly — integers and real numbers have completely different data representations at run-time, so the compiler must generate conversion code (a "cast") to adapt the number value before it is stored. Sometimes this is possible, sometimes not. A kind \(K\) is "compatible" with \(L\) if it is. Clearly conformance implies compatibility, but not vice versa.

§9. The kind object is of great significance to Inform, partly for historical reasons, partly because run-time code represents object values in a unique way. The lattice of subkinds of object is very well-behaved, in that any two subkinds will always be compatible. All of this means that object plays a unique role in Inform's kind hierarchy.

But not to us. In the kinds module, object is a kind like any other. It need not even exist.

§10. Kind variables. The 26 letters A to Z, written in upper case, can serve as kind variables — placeholders for kinds.3 In practice A is best avoided because it looks too much like an indefinite article, but it's very rare to need more than two.4 Phrase definitions in the standard Inform extensions use only K and L.

The meaning of text like "list of K" depends on context. If K is currently set to, say, number, then "list of K" means list of number; if it has no current setting, then K remains a placeholder and the result is list of K. Note that:

§11. The kinds-test REPL. The kinds module provides the Inform type system as a stand-alone utility, and one way to toy with it in isolation is to run test "programs" through the kinds-test tool. This is like a calculator, but for kinds and not values. A "program" is a series of descriptions of kinds, and the output consists of their evaluations. As a simple example: 

'number': number
'list of texts': list of texts
'phrase number -> text': phrase number -> text
'arithmetic value': arithmetic value
'relation of numbers to truth states': relation of numbers to truth states
'relation of numbers to numbers': relation of numbers

This is more of a test than it appears. In each line kinds-test has read in the textual description in quotes, parsed it into a kind object using the <k-kind> Preform nonterminal, then printed it out with Kinds::Textual::write (or in fact by using the %u string escape, which amounts to the same thing).

§12. In kinds-test, the 26 variables are initially unset, but can be given values by writing K = number, or similar. For example: 

'Q': Q
'list of relations of Q to R': list of relations of Qs to Rs
'substitute number for Q in Q': number
'substitute number for Q in list of Q': list of numbers
'substitute number for Q in list of relations of Q to Q': list of relations of numbers
'X = relation of Y to Y': relation of Ys
'X is definite?': false
'X = relation of numbers to numbers': relation of numbers
'X is definite?': true

§13. Overview of facilities. A kind is represented by a kind * pointer. These actually point to small trees of kind objects — see kinds — because many kinds are constructed out of others: thus list of texts is the result of applying the "list of ..." construction to the kind text.5 Kinds not constructed from other kinds are called "base kinds". Briefly: 

    Kinds::unary_con(CON_list_of, K_number)
    Kinds::binary_con(CON_relation, K_number, K_text)