Zig is a newer language that is only on version 0.16.0. Despite it not being at version 1.x yet and therefore could have major breaking changes, there is a lot to get excited about with the current implementation of the language. It shows such promise that I’m learning it now and hope for it to become a regular member of my toolbox. Here’s what excites me about it:

Type System Sanity

I’m a very big fan of Programming Language Theory (PL Theory) and of course that means type-systems and how to encode guarantees into the types. Part of that is having the actual type system be sane and detailed enough that you can represent those requirements and prevent users (including yourself) from breaking those requirements. Zig has an advanced metaprogramming technique called comptime that I will discuss later. But part of why comptime works well is that the underlying system it builds on is sane.

Non-Atomic Variables

  var1: [t1 -> v1; t2 -> v2]

where var1 is the name of the variable, tx are timestamps, and vx are the values of the variable at those timestamps.

Note that t(n+1) must be greater than t(n)

Domains

Domains are separate spheres of execution. Each thread would have their own Domain, for instance.

Frontier

Domains have a frontier, which establishes which variables it can see at which timestamp.

  d1: [var1 -> t1; var2 -> t3; var3 -> t7]

where d1 is the name of the domain, varx are variable names, and tx are timestamps

Unification Algorithm

    type term =
    | Var of string
    | Term of string * term list

You either have a type variable with a name, or a type constructor with a name and a list of argument

Unification takes a list of term pairs which have to be made matching.

Unification returns a list of substitutions, where a substitution is a pair of a string and a term, aka the variable name that should be substituted with the term.

Steps for unifying two terms

Try to match