TypOS

being an operating system for typechecking processes

Are the processes being typechecked? Are the processes doing the typechecking? Yes.

Still very much in the early stages of construction (may it never leave them!), TypOS is a domain-specific language for implementing type systems, based on an actor model (caveat emptor) of concurrent execution. Each region of source code is processed by an actor, implementing a typing judgement with a clearly specified interaction protocol. Actors may spawn other actors: child processes which correspond to the premises of typing rules. Actors communicate with one another along channels, in accordance with their stated protocol.

More details in this TYPES talk .

Installation

You will need to have the GHC Haskell compiler and the cabal tool on your system. To install, clone the repository, and execute

make install

This should give you a typos executable to run.

What's in a TypOS program?

1. descriptions of syntaxes
2. declarations of judgement interaction protocols
3. definitions of judgement actors
4. example invocations of judgement actors

And when you press go, you get to watch the execution trace of your examples, as control flits about between a treelike hierarchy of actors, making progress wherever possible. We are still at a rudimentary stage: there is a lot which remains to be done.

What gets typechecked?

We have a very simple syntax for the stuff that gets processed by TypOS actors.

A name begins with an alphabetical character, followed by zero or more characters which are alphabetical, numeric or _. Names are used in two ways:

• as variables, x, once they have been brought into scope
• as atoms, 'x, whose role is to be different from each other

We build up structure by means of

• binding: \x. term is a term which brings x into scope in term
• pairing: [ term | term ] is a term with two subterms

There is a special atom, [] (pronounced "nil"), and we adopt the bias towards right-nesting which has been prevalent since LISP established it in the 1950s. That is, every occurrence of |[ may be removed, provided its corresponding ] is removed also. It is typical, therefore, to build languages with terms of the form ['tag subterm .. subterm].

Now, there is no particular ideological significance to this choice of LISP-with-binding. It is a cheap way to get started, but it is not an ideal way to encode languages with more complex scoping structure. When we need more, we shall review this choice.

Of course, LISP-with-binding is intended merely as a substrate: not all terms are expected to be meaningful in all situations. We provide various means of classification. Let us begin.

syntax declarations

We start with a basic notion of context-free grammar. A syntax declaration allows a bunch of nonterminal symbols to be mutually defined. Here is an example, being a bidirectional presentation of simply typed lambda-calculus.

syntax
  { 'Check = ['Tag  [ ['Lam ['Bind 'Synth 'Check]]
                      ['Emb 'Synth] ]
             ]
  ; 'Synth = ['Tag  [ ['Rad 'Check 'Type]
                      ['App 'Synth 'Check] ]
             ]
  ; 'Type = ['EnumOrTag ['Nat ]
                        [ ['Arr 'Type 'Type] ]
            ]
  }

What are we saying? The terms you can 'Check can be lambda-abstractions but we also 'Embed all the terms whose type we can 'Synthesize. The latter comprise what we call 'Radicals (checkable terms with a type annotation) and 'Applications where a synthesizable function is given a checkable argument. E.g., the identity function might be written ['Lam \x. ['Emb x]].

How have we said it? Following the keyword syntax is a {;}-list of equations, each defining an atom by a term which happens to be a syntax description. You can see some components of syntax descriptions:

• ['Tag .. ] takes a list of pairs of atoms with lists of syntax descriptions, allowing us to demand exactly a list whose head is a tag and whose other elements are specified in a manner selected by the tag. So 'Lam and 'Emb are the tags for 'Check terms, 'Rad' and 'App for 'Synth terms.
• ['EnumOrTag .. ] takes two lists: the first one enumerates the permissible atoms, that is, it admits any of of them, whereas the second again is a list of pairs of tags and syntax descriptions (in fact, ['Tag ts] is syntactic sugar for [EnumOrTag [] ts ]; similarly ['Enum es ] is syntactic sugar for [EnumOrTag es [] ]). So Nat on its own is a 'Type, and 'Arr is a tag demanding two further types.
• Names of syntax declarations can occur recursively in syntax descriptions: these are atoms which is the name of a syntax, including the syntaxes defined in previous syntax declarations, or the current syntax declaration. E.g., we see that the 'Emb tag should be followed by one 'Synth term, while the 'Arr tag should be followed by two 'Types.
• ['Bind ..] specifies a term of form \x.t. It takes an atom which determines the named syntax to which the x is being added, then a syntax description for the t.

Correspondingly, in our example above, the x is classified as a 'Synth term, and so must be 'Embedded as the 'Checkable body of the 'Lambda abstraction.

The other permitted syntax descriptions are as follows:

• ['Nil] admits only [].
• ['Cons head tail] admits pairs [h|t] where head admits h and tail admits t.
• ['NilOrCons head tail] admits the union of the above two.
• ['Atom] admits any atom.
• ['AtomBar *as*] admits any atom, except those listed in as.
• ['Fix \x. ..] takes a syntax description in which the bound x is treated as a syntax description, allowing local recursion.
• ['Wildcard] admits anything.

For a more exciting example, we take

syntax { 'Syntax = ['EnumOrTag
  ['Nil 'Atom 'Wildcard 'Syntax]
  [['AtomBar ['Fix \at. ['NilOrCons 'Atom at]]]
   ['Cons 'Syntax 'Syntax]
   ['NilOrCons 'Syntax 'Syntax]
   ['Bind ['EnumOrTag ['Syntax] []] 'Syntax]
   ['EnumOrTag ['Fix \at. ['NilOrCons 'Atom at]]
               ['Fix \cell. ['NilOrCons ['Cons 'Atom ['Fix \rec. ['NilOrCons 'Syntax rec]]] cell]]]
   ['Enum ['Fix \at. ['NilOrCons 'Atom at]]]
   ['Tag ['Fix \cell. ['NilOrCons ['Cons 'Atom ['Fix \rec. ['NilOrCons 'Syntax rec]]] cell]]]
   ['Fix ['Bind 'Syntax 'Syntax]]]]
}

as the syntax description of syntax descriptions, using 'Fix to characterize the lists which occur in the ['AtomBar ..], ['Tag ..] and ['Enum .. ] constructs.

Judgement forms and protocols

Before we can implement the actors which process our terms, we must say which actors exist and how to communicate with them. Our version of Milner's judgement-form-in-a-box names is to declare name : protocol. A protocol is a sequence of actions. Each action is specified by

1. ? for input, $ for subject, or ! for output, followed by
2. the intended syntax description for that transmission, then
3. . as a closing delimiter.

A subject is an untrusted input whose validity the judgement is intended to establish. Morally, when you send a subject, you also receive trust in that subject. If this trust has been misplaced, then it has at least been displaced.

For our example language, we have

<!-- ``` ctxt |- 'Synth -> 'Type ``` -->

type  : $'Type.
check : ?'Type. $'Check.
synth : $'Synth. !'Type.

indicating that

• type actors receive only a 'Type subject;
• check actors receive a 'Type, which they may presume is already valid, and a 'Checkable term as a subject to check against the type; and
• synth actors receive a 'Synthesizable term as subject, then (we hope) transmit the (valid, we should ensure) 'Type synthesized for that term.

Our protocols are nowhere near as exciting as session types, offering only a rigid sequence of actions to do (or die). For the moment, the properties of inputs that actors rely on, and the properties of outputs that actors guarantee, are not documented, let alone enforced. In the future, we plan to enrich the notion of protocol with contracts for every signal which is not the subject. A contract should specify a judgement of which the signal is the subject. For the above, we should let check rely on receiving a 'Type which type accepts, but demand that synth always yields a 'Type which type accepts.

That is, we plan to check the checkers: at the moment we check that actors stick to the designated interleaving of input and output operations, and that syntax descriptions are adhered to. Subjects can be marked as such, and are checked to be transmitted only from client to server.

TypOS actors

An actor definition looks like judgement@channel = actor. The channel is the actor's link with its parent (so we often call it p) along which it must follow the declared protocol. Here is a simple example:

type@p = p?ty. case $ty
  { 'Nat ->
  ; ['Arr S T] ->
      ( type@q. q!S.
      | type@r. r!T.
      )
  }

This actor implements type, with channel p to its parent. Its first action is p?ty. to ask its parent for an input, which comes into scope as the value of the actor-variable ty. I.e., a receiving actor looks like channel?actor-variable. actor, which performs an input on the given channel, then continues as the actor with the actor-variable in scope. Actor variables stand for terms, and may be used in terms as placeholders. Our actor has received a type to validate. How does it proceed?

It performs a case analysis on the structure of the type. The actor construct is case scrutinee { pattern -> actor ; ..}. We shall specify scrutinees and patterns in more detail shortly, but let us continue the overview. The `'Na