Andreas Rossberg defined a concise and elegant type system for the concatenative language Cat created by Christopher Diggins that makes clear, once and for all, that the nature of the paradigm is solidly functional, point-free and higher order in a way that, as John Nowak remarks, goes beyond the original conception of Backus' FP. Here I wish to contribute to fixing these important ideas by presenting an extremely simple yet complete type inferencer for Cat. The idea is to show the most clear program I'm capable of, valuing above all purity and clarity and eschewing all performance considerations. I follow both the original definition in LtU and the Cat paper linked above.
As is usual with OCaml, there's a tension between a literate style of programming and the mandates of the forward-only definitions in a program module. This is why I choose to do away with the important but ultimately irrelevant minutiae, and proceed to the core of the program. These definitions are important but part of my personal prelude, so I present them first instead of at the point of their first usage so as to get them out of the way.
f % g is the composition of functions f and g. f $ x is the application of argument x to function f. thread applies f to the corresponding projections of its pair arguments.
let (%) f g x = f (g x)
let ($) f x = f x
let thread f (a, x) (b, y) = (f a b, f x y)
Some of the latter functions require operating on sets of variables, substitutions and the like. The big advantage of using lists to represent sets is that they are polymorphic for free, by using [Pervasives.compare]. If the expected number of elements is rather small, they are not too terribly inefficient. The union-as-merge algorithm to find the union of lists l and r is absolutely standard.
let rec union l r = match l, r with
| [], xs | xs, [] -> xs
| x :: xs, y :: ys ->
let c = compare x y in
if c < 0 then x :: union xs r else
if c > 0 then y :: union l ys else
x :: union xs ys
Typing
The type system devised by Andreas Rossberg is two-kinded: one kind for "atomic" types, and another for row types. The intention is that row types capture the entire program stack, while atomic types capture individual elements of it. This makes not only for a simpler presentation but also for a strictly consistent definition at the abstract syntax level, backed up by the types. The counterpart of this rigor is that structural recursion is duplicated for each kind.
The base atomic types are TInt, the type of numbers, and TBol, the type of truth values. The type of functions is TArr (r, r'). Since functions affect the whole program stack, both the source r and target r' types are row types. Type variables TVar n represent any type, and are implicitly universally quantified. The reason for this will be clear when I show the typing rules; suffice to say that, as John Nowak keenly remarks over at Reddit, the only values in a pure concatenative language are point-free functions, and so there is no need nor any way to use binders to introduce polymorphism, and types like ∀α.α that aren't inhabited actually are impossible. For this reason and simplicity in handling, variables are "named" as integers. They don't correspond to De Bruijn indices, as there is no binding construct in this type system.
The row types are RRow (r, t) describing a stack with the atomic type t on top, and the rest represented by the row type r. Much like with atomic type variables, a row type variable is represented by RVar n, with integer "name" n.
type ttyp = TInt | TBol | TArr of rtyp * rtyp | TVar of int
and rtyp = RRow of rtyp * ttyp | RVar of int
An integer representation of variables is too low-level for human consumption, however. There is a simple map: given a stock alpha of variable letters, select one in ascending order of index, adding primes and wrapping around each time the list of letters runs off.
let string_of_var alpha =
let card = String.length alpha in fun i ->
let k = i / card in
let c = String.make (k + 1) '\'' in
c.[0] <- alpha.[i - k * card]; c
For consistency with the original definition, atomic type variables are represented by lowercase letters, and row type variables are represented by uppercase letters.
let string_of_tvar = string_of_var "abcdefghijklmnopqrstuvwxyz"
and string_of_rvar = string_of_var "ABCDEFGHIJKLMNOPQRSTUVWXYZ"
Most of the functions that recur on the structure of atomic types are paired up with a companion that recurs on the structure of row types. As noted above, this pattern will be the norm in what follows, dictated by the realities of having to do structural recursion on two different ADTs. One of the most immediately useful such pair is a pretty printer. In the absence of an accompanying parser it's an arbitrary choice how to fix precedence for the different type constructors; however, the goal would have to be minimizing the number of parentheses required to print a type. I chose the arrow constructor to bind less strongly than the row constructor, whereas the original presentation appears to use a fully-parenthesized format. Note that the row constructor associates to the left: A x y means (A x) y by definition. The arrow is not really associative, as both the source and the target are row types, so there is no type A → (B → C).
The simplest arrow types beyond A → A are A x → A and A → A x neither of which requires parenthesizing to improve readability. A type that does require them according to our rules is A → A (B → B) (the type of the empty quote []).
let rec pp_print_ttyp pp t =
match t with
| TInt -> Format.pp_print_string pp "int"
| TBol -> Format.pp_print_string pp "bool"
| TVar v -> Format.pp_print_string pp (string_of_tvar v)
| TArr (t, t') ->
Format.fprintf pp "@[<hov 1>(%a@ ->@ %a)@]"
pp_print_rtyp t pp_print_rtyp t'
and pp_print_rtyp pp t =
let rec go pp = function
| RVar v -> Format.pp_print_string pp (string_of_rvar v)
| RRow (t, t') ->
Format.fprintf pp "%a@ %a"
go t pp_print_ttyp t'
in
Format.fprintf pp "@[<hov>%a@]" go t
I don't usually install the printers early in the development, as the prettyfication may mask or hide information important for the algorithms but irrelevant for the user. In this case, the concrete syntax is in one-to-one correspondence with the abstract syntax, so that there's no harm done in issuing:
#install_printer pp_print_ttyp ;;
#install_printer pp_print_rtyp ;;
in the interpreter. To convert a formatter into a string builder, the following function is handy:
let string_of_formatter pp =
Format.flush_str_formatter % pp Format.str_formatter
Substitutions
Substitutions of types for variables are made simpler by the use of integer names (so that renaming is an arithmetic operation), but a little different from the usual presentation in that there are no binders, or rather, all variables are implicitly bound by universal quantifiers. That implies that, in order to avoid capture, the variables in the substitute must be renamed to avoid clashes with those in the substituend. In order to rename those variables, it is necessary to know first which are the variables in need of renaming. As it's clear from the above, the answer is all of them, as each and every one is technically free.
Since the kinds of atomic and row types are distinct, the variables must be kept apart and treated separately. Instead of introducing a union type, I prefer to work with split contexts:
let rec free_vars_ttyp = function
| TInt | TBol -> [], []
| TVar v -> [v], []
| TArr (t, t') -> thread union (free_vars_rtyp t) (free_vars_rtyp t')
and free_vars_rtyp = function
| RVar v -> [], [v]
| RRow (t, t') -> thread union (free_vars_rtyp t) (free_vars_ttyp t')
(thread here applies union componentwise to the resulting pairs). This next function is the workhorse of the section. A substitution of term s for variable v in t proceeds by straightforward structural recursion. The simplest case is to start from an unsafe substitution and build from there. To avoid capturing free variables in the substitute, it is necessary to perform a generalized renaming on the substituend. This is carried out by the so-called generalize instance operation which I'll show later, which ensures that I can get away with unsafe substitutions without the need to finesse the rebinding too much, since it is done consistently to all the variables in a type.
Substitution comes in four versions, two for each kind of substitute, two for each kind of substituend:
let rec substitute_tvar_ttyp s v t = match t with
| TArr (t, t') -> TArr (substitute_tvar_rtyp s v t, substitute_tvar_rtyp s v t')
| TVar w when v = w -> s
| _ -> t
and substitute_rvar_ttyp s v t = match t with
| TArr (t, t') -> TArr (substitute_rvar_rtyp s v t, substitute_rvar_rtyp s v t')
| _ -> t
and substitute_rvar_rtyp s v t = match t with
| RRow (t, t') -> RRow (substitute_rvar_rtyp s v t, substitute_rvar_ttyp s v t')
| RVar w when v = w -> s
| _ -> t
and substitute_tvar_rtyp s v t = match t with
| RRow (t, t') -> RRow (substitute_tvar_rtyp s v t, substitute_tvar_ttyp s v t')
| _ -> t
Now, as I'll show later, unification proceeds by finding a pair of lists of substitutions (ts, rs), with the first substitution to apply at the end. For this I need to apply substitutions from right to left, and so I need a right fold on the lists. Instead of substituting in parallel, I sequence the substitutions, even if they are independent. This pattern is nicely captured by composition of right folds.
let substitute_ttyp (ts, rs) =
List.fold_right (fun (v, s) t -> substitute_tvar_ttyp s v t) ts
% List.fold_right (fun (v, s) t -> substitute_rvar_ttyp s v t) rs
and substitute_rtyp (ts, rs) =
List.fold_right (fun (v, s) t -> substitute_tvar_rtyp s v t) ts
% List.fold_right (fun (v, s) t -> substitute_rvar_rtyp s v t) rs
With this I can build the other important structural operation on types, the so-called generalize instances mentioned above and required for capture-free unification. This operation forces all variables in the unificand to be fresh. An inefficient but simple way to rename is to do it relative to a context listing all the "used" variables, and finding the next variable that doesn't clash with that context.
This finds the next unused variable in a set l:
let next_unused_var l = 1 + List.fold_left max 0 l
This maps a list by indexing each element in it. It is equivalent to the Haskell zipWith f \[0..\]:
let rec map_indexed f i = function
| [] -> []
| x :: xs -> f i x :: map_indexed f (succ i) xs
Given a pair of contexts, renaming a type relative to them is simple enough: map free type variables to increasingly large names starting from the next unused variable in each context. The function below abstracts the details of both type kinds and builds a map to rename free type variables (tf, rf) relative to both halves of the context (ts, rs):
let gen_instance (ts, rs) (tf, rf) =
map_indexed (fun i x -> x, TVar i) (next_unused_var ts) tf,
map_indexed (fun i x -> x, RVar i) (next_unused_var rs) rf
let gen_instance_ttyp ctx t =
substitute_ttyp (gen_instance ctx (free_vars_ttyp t)) t
and gen_instance_rtyp ctx t =
substitute_rtyp (gen_instance ctx (free_vars_rtyp t)) t
After this, the following functions are straightforward. These checks if the variable v occurs in type t and will be needed next:
let rec occurs_tvar v t =
let rec go v = function
| RRow (t, t') -> go v t || occurs_tvar v t'
| _ -> false
in match t with
| TVar w -> v = w
| TArr (t, t') -> go v t || go v t'
| _ -> false
let rec occurs_rvar v = function
| RVar w -> v = w
| RRow (t, TArr (t', t'')) ->
occurs_rvar v t
|| occurs_rvar v t'
|| occurs_rvar v t''
| RRow (t, _) -> occurs_rvar v t
Unification
The following algorithm is standard and is a variant of the one shown in Pierce's Types and Programming Languages. Type errors are reported in the most crude fashion possible:
exception Type_error of string
Unification between terms t and t' proceeds by finding a list σ of substitutions x → t such that σt = σt'. The simplest way to build such a substitution list is to carry it around as an accumulating parameter subs. The only real work is to ensure that at all points the terms to be compared are subjected to the current substitution, and recurring on the structured terms:
let rec unify_ttyp (ts, rs as subs) t t' =
if t == t' then subs else
let t, t' = substitute_ttyp subs t, substitute_ttyp subs t' in
match t, t' with
| TVar v, t ->
if not (occurs_tvar v t) then ((v, t) :: ts, rs) else
raise (Type_error "occurs check in simple type")
| t, TVar v ->
if not (occurs_tvar v t) then ((v, t) :: ts, rs) else
raise (Type_error "occurs check in simple type")
| TArr (s, t), TArr (s', t') ->
unify_rtyp (unify_rtyp subs s s') t t'
| _ -> raise (Type_error "simple type mismatch")
and unify_rtyp (ts, rs as subs) t t' =
if t == t' then subs else
let t, t' = substitute_rtyp subs t, substitute_rtyp subs t' in
match t, t' with
| RVar v, t ->
if not (occurs_rvar v t) then (ts, (v, t) :: rs) else
raise (Type_error "occurs check in row type")
| t, RVar v ->
if not (occurs_rvar v t) then (ts, (v, t) :: rs) else
raise (Type_error "occurs check in row type")
| RRow (s, t), RRow (s', t') ->
unify_ttyp (unify_rtyp subs s s') t t'
| _ -> raise (Type_error "row type mismatch")
This is my absolutely favorite algorithm, and all that is needed to implement the typing rules of the language.
The initial environment defines the types of the built-in primitives, as defined in the Cat paper:
let initial_env =
let r, s, t, u = RVar 0, RVar 1, RVar 2, RVar 3
and x, y = TVar 0, TVar 1 in
[
"succ" , TArr (RRow (r, TInt), RRow (r, TInt));
"pred" , TArr (RRow (r, TInt), RRow (r, TInt));
"neg" , TArr (RRow (r, TInt), RRow (r, TInt));
"add" , TArr (RRow (RRow (r, TInt), TInt), RRow (r, TInt));
"sub" , TArr (RRow (RRow (r, TInt), TInt), RRow (r, TInt));
"lteq" , TArr (RRow (RRow (r, TInt), TInt), RRow (r, TBol));
"pop" , TArr (RRow (r, x), r);
"dup" , TArr (RRow (r, x), RRow (RRow (r, x), x));
"swap" , TArr (RRow (RRow (r, x), y), RRow (RRow (r, y), x));
"eval" , TArr (RRow (r, TArr (r, s)), s);
"dip" , TArr (RRow (RRow (r, x), TArr (r, s)), RRow (s, x));
"if" , TArr (RRow (RRow (RRow (r, TBol), TArr (r, s)), TArr (r, s)), s);
"while" , TArr (RRow (RRow (r, TArr (r, r)), TArr (r, RRow (r, TBol))), r);
"constantly", TArr (RRow (r, x), RRow (r, TArr (s, RRow (s, x))));
"compose" , TArr (RRow (RRow (r, TArr (s, t)), TArr (t, u)), RRow (r, TArr (s, u)));
]
If you want to see "nice types", you can do:
List.map (fun (n, t) -> n, string_of_formatter pp_print_ttyp t) initial_env ;;
Terms
Terms come into a few simple forms, and this is one half of the "essence" of concatenative programming. An atomic program is either the empty program E, an integer constant I n, a truth value B b or a named primitive P id. A composite term is a quotation Q t or an application A (t, t') of term t to term t':
type term = E | I of int | B of bool | P of string | Q of term | A of term * term
A pretty-printer comes handy to have a clear representation of a term:
let rec pp_print_term pp t = match t with
| E -> ()
| I n -> Format.pp_print_int pp n
| B b -> Format.pp_print_string pp (if b then "true" else "false")
| P s -> Format.pp_print_string pp s
| Q t -> Format.fprintf pp "@[<hov 1>[%a]@]" pp_print_term t
| A (t, u) ->
Format.fprintf pp "@[<hov>%a@ %a@]"
pp_print_term t pp_print_term u
Remember that in a concatenative language every term is a function and juxtaposition is composition. This means that many reconstructed types require lifting to functions from rows to rows:
let quote_tvar t =
let v = RVar (next_unused_var (snd (free_vars_ttyp t))) in
TArr (v, RRow (v, t))
And now for the second half —and finale— of the "essence" of concatenative programming. This function implements Rossberg's syntax-directed type reconstruction for Cat. The empty program has the identity effect on stacks. Constant are lifted to stack effects. A primitive derives its type from the current environment, which in this case is initial and constant. An application requires verifying that both terms are functions. As is clear from the other rules, the only way it can fail to be an arrow is if the environment registers a "bogus" type. Relative to a well-typed initial environment, every concatenative program is a function. This is a theorem that has an immediate proof by structural recursion on the typing rules.
In order to unify the target of the first arrow with the source of the second, the latter's type variables must be generalized relative to the free variables of the former. With that, the resulting type is built from the substitution applied to source and target of the types being typechecked:
let rec typecheck = function
| E -> let v = RVar 0 in TArr (v, v)
| I n -> quote_tvar TInt
| B t -> quote_tvar TBol
| Q q -> quote_tvar (typecheck q)
| P n ->
begin
try List.assoc n initial_env
with Not_found -> raise (Type_error ("Unbound value "^n))
end
| A (q, q') ->
let t = typecheck q
and t' = typecheck q' in
match t, t' with
| TArr (r, s), TArr _ ->
let TArr (r', s') = gen_instance_ttyp (free_vars_ttyp t) t' in
let subs = unify_rtyp ([], []) s r' in
TArr (substitute_rtyp subs r, substitute_rtyp subs s')
| _ -> raise (Type_error "The types fail to compose")
To bring this program to a close, here's Andreas' original example:
# typecheck (A (Q (I 42), A (Q (P "add"), P "compose"))) ;;
- : ttyp = (E -> E (D int -> D int))
