possum

I'm writing possum because I can.

It's a rendering into code of a collection of heartfelt prejudices about type systems and type checking and synthesis, primarily related to telling the difference between them.

stuff

The raw stuff in which possum trades is a LISP-like syntax which distinguishes things we expect to check and things from which types (or whatever) will be synthesized. We expect to check canonical (or introduction) forms and synthesize neutral (or elimination) forms.

I haven't made my mind up about syntax yet, and probably never will. Abstractly, however we have

canonical terms

• atoms are identifiers that can be told apart; there is a distinguished atom 'nil', written [] if at all;

• cons cells look like [ term0 . term1 ]; standard right-nesting prejudices apply, so that .[ blether ] may just be written as blether;

• abstractions look like \ variable term where variable is an identifier that locally stops being available as an atom, so don't shadow any of the atoms you care about

neutral usages

• variables, as introduced by abstractions

• eliminations, being usage thing, indicating some computational task

However, we may also change direction in two ways.

• a usage can become a term; unless it is a variable, you had better write it like ( usage ), and indeed, any term in parentheses is taken to be a usage

• a term can become a usage if it is given a classifier, thus term : Term; we call such a usage a radical; radicals embedded into things have their classifiers erased

metavariables

Brace yourselves! I mean it. { metavar usage ... usage } is the syntax for invoking a metavariable. Metavariables can stand for either a term or a usage.

patterns

A pattern is a question we can ask about the structure of a term. A positive answer amounts to an instantiation of the metavariables in the pattern, which must occur linearly, sorry Dad. The canonical components are built the same way as for stuff.

In addition, a pattern can be

• a variable introduced by an abstraction, matching only that variable;

• a metavariable { identifier dependencies } which binds the identifier as a metavariable and indicates upon which variables its instantiating term may depend, either by inclusion or exclusion; an inclusion is a list of variables separated by spaces; an exclusion is a sequence of spaces preceded by a \ (double duty!); but an empty inclusion includes everything and an empty exclusion excludes everything;

and it is sometimes ok to write

• a usage metavariable, which is ( identifier dependencies )

but it is often not a good idea to ask if a term is a usage, because that is not stable under substitution, and it is never a good idea to ask what sort of usage something is.

Remark: if we adjoin a bottom element to the patterns, representing the grumpy pattern which never matches anything, we find that patterns form a monoid whose neutral element is {x} and whose combining operation is unification.

judgement forms

A judgement form is specified as a sequence (preferably nonempty) of atoms, brackets and places. (Behind the scenes, it's going to turn into a pattern).

jform ::= jelt *

jelt ::= atom | [ jform ] | place | condition

place ::= { identifier } | ( identifier )

condition ::= { judgement ] | [ judgement }

Brace-places are for terms; Paren-places are for usages. Places may not occur consecutively. Neither : nor = may be used as an atom in a judgement form (at least, not by you: more later).

A condition is a judgement matching some previously declared judgement form: its bracketing is asymmetric because it points either left into the past (i.e., it's a precondition), or right into the future (a postcondition). The former tells you what you must check before you ask if the judgement holds. The latter tells you what you may trust after you are told that the judgement holds, in addition to the judgement itself, of course. The places scope over the conditions: there's more to it, of course, but I'll get there.

Judgement forms have some places which are designated as subjects. How is this designation done? If a place is not the subject of a condition then it is a subject of the form being specified. If it is the subject of a condition, then it must be the subject of only one condition: if that is a precondition, then we say that place is an input; if a postcondition, then an output.

It is common that judgement forms have at most one subject. It is thus tidy to support the notation that an input place governed by one-subject precondition or an output place governed by a one-subject postcondition can be replaced by the condition itself. For (thank goodness) example:

judgement type {T}
judgement {type T] :> {t}
judgement (e) <: [type S}

The above specifies three judgement forms. The first has but a subject, a term, which we are judging to be a type. The second also judges a term, with respect to another term already required to be a type. The third judges a usage, yielding a term which is promised to be a type.