How to think about typing inference rules when thinking about typechecking?

Question

I am trying to build an imperative programming language with a type system that will allow for proofs. I just found kind lang, which implements all the ideas that I have been meaning to use (plus more), but it is a functional language. An older rendition of the project was Formality in JavaScript, or probably earlier, the Calculus of Constructions in JavaScript. Also I take inspiration from Rust.

The key function I am trying to understand is how typechecking works (also, how type inference works / is implemented). From Formality, it is like this basically (from the link):

const Var = (name,indx)                => ({ctor:"Var",name,indx});
const Ref = (name)                     => ({ctor:"Ref",name});
const Typ = ()                         => ({ctor:"Typ"});
const All = (eras,self,name,bind,body) => ({ctor:"All",eras,self,name,bind,body});
const Lam = (name,body)                => ({ctor:"Lam",name,body});
const App = (func,argm)                => ({ctor:"App",func,argm});
const Let = (name,expr,body)           => ({ctor:"Let",name,expr,body});
const Def = (name,expr,body)           => ({ctor:"Def",name,expr,body});
const Ann = (done,expr,type)           => ({ctor:"Ann",done,expr,type});
const Nat = (natx)                     => ({ctor:"Nat",natx});
const Chr = (chrx)                     => ({ctor:"Chr",chrx});
const Str = (strx)                     => ({ctor:"Str",strx});

// ...

function typecheck(term, type, defs, ctx = Nil()) {
  var typv = reduce(type, defs);
  switch (term.ctor) {
    case "Lam":
      if (typv.ctor === "All") {
        var self_var = Ann(true, term, type);
        var name_var = Ann(true, Var(term.name, ctx.size+1), typv.bind);
        var body_typ = typv.body(self_var, name_var);
        var body_ctx = Ext({name:term.name,type:name_var.type}, ctx);
        typecheck(term.body(name_var), body_typ, defs, body_ctx);
      } else {
        error(term, ctx, "Lambda has a non-function type.");
      }
      break;
    case "Let":
      var expr_typ = typeinfer(term.expr, defs, ctx);
      var expr_var = Ann(true, Var(term.name, ctx.size+1), expr_typ);
      var body_ctx = Ext({name:term.name,type:expr_var.type}, ctx);
      typecheck(term.body(expr_var), type, defs, body_ctx);
      break;
    default:
      var infr = typeinfer(term, defs, ctx);
      var eq = equal(type, infr, defs, ctx.size);
      if (!eq) {
        var type0_str = show(normalize(type, {}), ctx);
        var infr0_str = show(normalize(infr, {}), ctx);
        error(term, ctx, 
          "Found type: \x1b[2m"+infr0_str+"\x1b[0m\n" +
          "Instead of: \x1b[2m"+type0_str+"\x1b[0m");
      }
      break;
  };
  return {term,type};
};

So there's that, and then there are things like this ("typing rules"):

How am I to read these typing rules, and yet think about a type checking algorithm? I would like to (in my head at least) convert the typing rules to useful code. Basically, what is a type rule for in the end? How does it get used in a type checking algorithm? How do I read the typing rule so that it makes sense in the context of a type checking algorithm pretty much? What is the relation between type inference rules and type checking? I don't see how to combine the two clearly and practically.

Answer 1

The rules of a type system may be given in one of several ways.

We often begin by defining a relation "term $t$ has type $A$" using rules of inference without giving any particular way of turning the rules into an algorithm. This is sometimes called the "declarative style". The declarative style is usually the easiest to understand and most amenable to mathematical treatment, such as semantics. If you're designing a new type system you'd probably start here in order to not get tangled up in various algorithmic details.

We then want an equivalent formulation that indicates how we are supposed to carry out type checking. This is sometimes called "algorithmic style".

One particular kind of algorithmic style are the "syntax directed rules" – by which we mean that we can tell which rule to use by analyzing the syntax of the term $t$ that we are trying to typecheck. This is good because it tells you how to implement typechecking. Most of the time most declarative rules are already syntax-directed – but in interesting cases there are always a couple that are not.

It takes experience to know how to design an algorithmic style that correspond to a given declarative style. In fact, figuring out a good type-checking algorithm for a new type system may be quite challenging and publication-worthy.

A popular way to formulate type systems in algorithmic style is to split the relation "$t$ has type $A$" into two:

• check that $t$ has the given type $A$, and
• infer (synthesize, compute) the type of $t$

This is known as a bidirectional type system. The checking and inferring relations (also called phases) are often mutually recursive, and they are also syntax directed – so they give an algorithm. (In case it is not clear, the algorithm is simply to look at the syntactic structure of $t$ to find out which rule should be used, more or less.)

There are many other kinds of algorithms that perform type checking and type inference. For instance, they may collect a set of equational constraints that needs to be solved. Or they may track some other information. It is traditional for such algorithms to be displayed using inference rules (rather than pseudocode that looks like Algol 68). The accompanying text will tell you which bits are to be thought of as inputs and which as outputs, and the rules will be syntax-directed so that in each situation at most one will apply. (And if none apply, you've got a type error.)

To answer your question specifically: there are a number of techniques that turn inference rules into algorithms. What is appropriate in your case depends on what your type system look like. Have you written it down? In declarative style?