6
$\begingroup$

I'm implementing my own statically-typed programming language and I'm not too happy with my own approach to types. At the moment, I'm relying on mapping a textual representation of a type to an index in a hash map, and then trying to parse that for "sub types" (for things like "arrays of a type", "pointers to arrays of a type", etc).

How do compiler implementations parse and represent types, in order to track them throughout the compilation process, compare them for equivalence as well as handle those variants or subtypes?

$\endgroup$
5
  • 1
    $\begingroup$ Welcome to PLDI! This seems like a pretty broad question, since there's sooo many variations in how type systems work, and so many different parts of them. Compiler design is a whole field, after all. $\endgroup$ May 17, 2023 at 15:13
  • 4
    $\begingroup$ That's fair. I got a little excited about this stack-exchange because I'm quite new to language implementation. I'd like to narrow down the question so it's useful, but I don't really know how best to. $\endgroup$ May 17, 2023 at 15:21
  • 1
    $\begingroup$ Could you please be more specific? Are you asking about type systems per se (e.g. type checking algorithms)? Compiler architecture (e.g. how to thread types through IRs)? How to parse and represent types as a data structure? $\endgroup$ May 17, 2023 at 16:26
  • $\begingroup$ I'm interested in all of that, really, but for this question, more the latter two. Parsing and representing types as a data structure within the compiler was my main focus though, so let's go that way $\endgroup$ May 17, 2023 at 16:41
  • 1
    $\begingroup$ Thanks for editing your question. I have voted to reopen. $\endgroup$ May 17, 2023 at 17:09

3 Answers 3

5
$\begingroup$

Types, like many other things in compilers (programs), are usually represented as some encoding of a discriminated union - similar to how we usually store and manipulate ASTs.

For example, suppose we were implementing a type checker for STLC (Simply Typed Lambda Calculus), extended with some integral arithmetic primitives. We start by thinking about what kinds of types our language will have, so we can go about representing them. For our flavour of STLC, we only really need a ground type for integer literals (e.g., 4 : int), some notion of type variables (unknowns, x : 't0), and arrow types (e.g., f : 't0 -> int).

In OCaml (or any other language with algebraic datatypes), we could do this very naturally:

type typ =
  | Tint
  | Tvar of int
  | Tarrow of typ * typ

In languages without ADTs, such as Java or C++, the common choice is to encode discriminated unions (tagged unions) as a class hierarchy, down-casting when necessary. For example, in Java we may have:

public abstract class Type {
  public class Int extends Type {}
  public class Var extends Type {
    private int name;
    public Var(int name) {
      this.name = name;
    }
    // ...
  }
  public class Arrow extends Type {
    private Type domain, codomain;
    public Arrow (Type domain, Type codomain) {
      this.domain = domain;
      this.codomain = codomain;
    }
    // ...
  }

}

In order to work with these encodings, we have pattern matching in OCaml and various methods in Java (instanceof, using a visitor design pattern, the modern switch, etc.).

let foo = function
  | Tarrow (l, r) -> (* ... *)
  | _ -> (* ...  *)
public void foo(Type ty) {
  if (ty instanceof Type.Arrow arrow) {
    // use arrow in some way
  }
}

The reason why people tend to enjoy writing compilers in OCaml, Haskell, Standard ML, etc. is that the encoding of recursive data (inductively defined) is incredibly convenient and the means by which to work with it (structural recursion) is very clean to express with pattern matching.

The troubles of dealing with recursive type abbreviations, type definitions that are not well founded, type equality, shadowed type definitions, etc. is usually up to book keeping. Of course, structural equality is not so difficult to implement, but many languages have a more strict notion of what it means for two types to be equal (within the type system).


Another thing to look out for is that type representations are quite often implemented in such a way to support a common operation performed on them in the context of type inference; destructive unification. So, their definitions are often augmented with constructors specifically for inducing a union-find forest (union-find is an ideal implementation strategy for the usual kinds of first-order unification we see in Hindley-Milner type systems).

If we look at the very approachable Caml Light codebase, we see its representation of types isn't too far from what I've described: Caml Light: compiler/globals.ml. We see that type variables (Tvars) hold a mutable reference cell that's mutated during destructive unification. It's typical that these union-find artefacts are removed after inference in a process sometimes called "zonking" (from the GHC codebase - effectively, replacing all annotated types with their representative).

Similarly, if we look at Clang, we'll see its clang::PointerType is a subtype of clang::Type and appears to store the type being pointed to, with a relevant accessor: getPointeeType() - we can imagine that the idiomatic encoding in an ML would be something like:

type typ =
  | (* ... *)
  | Pointer of typ

So, really: like many things in this area of programming, it tends to boil down to how your implementation language allows you to encode and work with one of the most important ideas in programming: discriminated unions. It is incredibly unfortunate that many mainstream languages neglected this concern until recently.

I hope this helps, it should be clear that many type formation rules can be encoded as inductive data structures in a fairly straightforward way. As for the other problems, those are largely bookkeeping (see the concept of "stamps" in the Caml Light and OCaml compilers).

$\endgroup$
5
  • $\begingroup$ Wow, this is a very comprehensive answer, thank you. I'm not quite sure about a few terms you use, though. "Destructive unification" and "union-find forest". Could you clarify those for me? $\endgroup$ May 18, 2023 at 4:23
  • $\begingroup$ Many type inference algorithms rely on unification for working out of two types are "compatible" (made equal up to a unifying substitution). Old unification algorithms such as that of Robinson's are incredibly inefficient for real world compilers (they reify substitutions as actual things to compose and apply), and so most make use of destructive unification (based on the union-find data structure, as a forest, encoded directly in the type representation). This is effectively the difference between algorithm J and algorithm W - J has a magic "unify" function that's taken to be done this way. $\endgroup$ May 18, 2023 at 6:41
  • 1
    $\begingroup$ I recommend introductory resources such as Oleg's telling of the core of the Caml Light/OCaml typechecker: okmij.org/ftp/ML/generalization/sound_eager.ml - the effective idea is that when you're dealing with polymorphism, where some constraint specialises a type variable, you can do the substitution implicitly as part of the union-find data structure. When we unify 'a with int, we really rewrite the cell representing the unbound type variable 'a to be a link to the representation of the type int. I recommend getting familiar with union-find, it's key to many fun algorithms. $\endgroup$ May 18, 2023 at 6:43
  • $\begingroup$ I appreciate the resource link. I have no experience with OCaml/Caml at all, so reading those sources is a bit challenging. $\endgroup$ May 18, 2023 at 12:22
  • $\begingroup$ This is an excellent answer, except for one point. This answer discusses rather simple type systems, such as Caml Light's (which is pretty much just Hindley-Milner). A lot of what you dismiss as “bookkeeping” is very much nontrivial. With features such as structural subtyping, modules and recursive types, the OCaml type checker is considerably more complex. With many advanced features, you can't have a canonical representation of types (or don't want to, because it would be unprintable in error messages). $\endgroup$ May 20, 2023 at 22:02
2
$\begingroup$

The easiest way to track type information---as well as identifier resolution---is by storing semantic information in the abstract syntax tree (AST). Some compilers refer to this semantically upgraded AST as the high-level intermediary representation (HIR).

As for how to compare types, the specifics depend heavily on your language's semantics. But let's say that your compiler's semantic analysis (sema) phase walks the AST to produce the HIR. Then for each step through the tree, you ask whether the user's action is permitted under your type rules. Eg., a function call is allowed because the function's type signature is met by the operands the user has provided. Any information gleamed from visiting that AST node is embedded in a new HIR node.

As for parsing types, treat your types the same way you would any other identifier. Your grammar should only see types the same way it sees variables; don't handle this during syntax. Let the sema phase determine the kind of identifier (type vs variable) and whether it was appropriate in the user's code.

Lastly, I will give a tip I learned the hard way... If you ever plan on lowering your AST/HIR to a mid-level IR (MIR) or to a virtual machine (VM) at some point in the future, just have the MIR/VM store its opcodes in the compiler's initial HIR at startup. I.e., the VM effectively creates the initial HIR so that the compiler can compare user calls against built-in functions against the VM's opcodes. Then the codgen phase only needs to emit those opcodes in addition to any resolved operands.

$\endgroup$
2
  • $\begingroup$ This covers how type information propagates through the AST. How would you represent the type (and it's properties?) Thinking about both composite/record types as well as something like the types in ML-style languages $\endgroup$ May 17, 2023 at 18:02
  • $\begingroup$ @springogeek: Depending upon the language, the AST may be a rather natural representation for the type, at least if one makes a few tweaks like constant folding and having an "user identifier" node contain a link to the definition. $\endgroup$
    – supercat
    Sep 29, 2023 at 22:08
2
$\begingroup$

Storing them in a dynamic array seems like a good idea in my language.

I have Crystal-like union typing in my language, so types can be arbitrarily large, and I needed to solve the issue of type storage.

If it's a hashmap, you'd have the HashMap type that takes two arguments: the Key Type and the Value Type. In a dynamic array, HashMap<string, int> can simply look like this: [TYPE_HASHMAP, TYPE_STRING, TYPE_INT]

Then you can just probe the list to figure out the type of something.

A function like this: fn foo(a: int, b: string) -> bool

Can look like this in a type list: [TYPE_FUNCTION, 2, TYPE_INT, TYPE_STRING, TYPE_BOOL]

If the types have subsub types, say a function like this fn foo(map: HashMap<string, Array<int>>) -> void

It can look like this: [TYPE_FUNCTION, 1, TYPE_HASHMAP, TYPE_STRING, TYPE_ARRAY, TYPE_INT, TYPE_VOID] (First the function type, with 1 argument, then the HashMap type, the hash map key type, the hash map value type which is an array with its value type as an int and finally the return type)

This makes it easy to compare equality through linear probing. It's easy to manage too I think. It's sort of like types can take arguments.

$\endgroup$
2
  • $\begingroup$ This is an interesting approach. I assume you aren't using an enum for types, because that would restrict your ability to create new types during compilation, right? $\endgroup$ May 17, 2023 at 19:27
  • $\begingroup$ Not necessarily. An enum can be converted to an integer in most languages so custom types use the same enums but within a user range, in my case it's between 15-60000. That way I can keep the size of individual types capped at 16 bits. $\endgroup$
    – Lucrecious
    May 20, 2023 at 1:56

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .