0
$\begingroup$

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"):

enter image description here

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.

$\endgroup$
2
  • 1
    $\begingroup$ Currently I am doing something similar using Prolog. I know you want to use an imperative programming language but if you can learn OCaml then "Types and Programming Languages" by Benjamin C. Pierce (WorldCat) might help you. Expect to spend a few months working through the book to get the most out of it. $\endgroup$
    – Guy Coder
    Jan 26, 2022 at 9:23
  • $\begingroup$ I would have given this an upvote but you noted imperative programming language. $\endgroup$
    – Guy Coder
    Jan 26, 2022 at 9:28

1 Answer 1

3
$\begingroup$

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?

$\endgroup$
6
  • $\begingroup$ Nice answer but is this a pretext to a paper? (Rhetorical question) In fact, figuring out a good type-checking algorithm for a new type system may be quite challenging and publication-worthy. $\endgroup$
    – Guy Coder
    Jan 26, 2022 at 9:26
  • $\begingroup$ No, it's just an observation about the programming language community. $\endgroup$ Jan 26, 2022 at 9:42
  • $\begingroup$ In my particular case I have a bunch of types written down in the language syntax, but don't yet know how to formulate things declaratively using type system notation. So in my case I am wondering, given a bunch of types like programming language types (typescript, for example), how do I parse the code and do typechecking... But I want to do it in a highly structured "official" way, like that algorithm I posted above (which seems to be applying the typing rules). So I want to know how to read (and soon write) the rules so I can do that for the language and implement a proper typechecker. $\endgroup$
    – Lance
    Jan 26, 2022 at 9:54
  • $\begingroup$ Have you read any textbooks, such as TAPL and PFPL? $\endgroup$ Jan 26, 2022 at 10:00
  • 1
    $\begingroup$ Examples of small typechecking and inference algorithms are available in the PL Zoo. $\endgroup$ Jan 26, 2022 at 10:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.