Two encodings of substitution operation

Substitution operations are heavily used in implementing type checkers. A substitution is a finite mappings from type variables to types. Thus it is natural to define Subst as a list of (Name, Type) pairs as in the following example.

import Data.Bifunctor

type Name = String

data Type = TVar Name
          | TCon Name [Type]

type Subst = [(Name, Type)]

Composition of substitutions can be encoded as operations over the underlying association list.

idSubst :: Subst
idSubst = []

composeSubst :: Subst -> Subst -> Subst
composeSubst s1 s2 = map (second (applySubst s1)) s2 ++ s1

applySubst applies the substitution given over the structure of the type replacing type variables as specified.

applySubst :: Subst -> Type -> Type
applySubst s (TVar n) = case lookup n s of
                          Nothing -> TVar n
                          Just t -> t
applySubst s (TCon n ts) = TCon n (map (applySubst s) ts)

Martin Grabm¨uller’s Algorithm W Step by Step uses a slight variation of this encoding to implement Hindley-Milner type system. His version uses Map Name Type instead of [(Name, String)] for efficient lookup.

Alternatively, we can encode substitution operations directly as a function from type variables to types.

type Subst = Name -> Type

idSubst :: Subst
idSubst n = TVar n

composeSubst :: Subst -> Subst -> Subst
composeSubst s1 s2 = applySubst s1 . s2

applySubst :: Subst -> Type -> Type
applySubst s (TVar n) = s n
applySubst s (TCon n ts) = TCon n (map (applySubst s) ts)

Simon Peyton Jones’s The Implementation of Functional Programming Languages uses this encoding of substitution to implement the type checker.

These two encodings are equivalent.