[A type system is a] tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.
— Benjamin Pierce
Type systems are a formal language in which we can describe and restrict the semantics of a programming language. The study of the subject is a rich and open area of research with many degrees of freedom in the design space.
As stated in the introduction, this is a very large topic and we are only going to cover enough of it to get through writing the type checker for our language, not the subject in its full generality. The classic text that everyone reads is Types and Programming Languages or ( TAPL ) and discusses the topic more in depth. In fact we will follow TAPL very closely with a bit of a Haskell flavor.
In the study of programming language semantics, logical statements are written in a specific logical notation. A property, for our purposes, will be a fact about the type of a term. It is written with the following notation:
These facts exist within a preset universe of discourse called a type system with definitions, properties, conventions, and rules of logical deduction about types and terms. Within a given system, we will have several properties about these terms. For example:
- (A1) 0 is a natural number.
-
(A2) For a natural number
$n$ ,$\mathtt{succ}(n)$ is a natural number.
Given several properties about natural numbers, we'll use a notation that will allow us to chain them together to form proofs about arbitrary terms in our system.
In this notation, the expression above the line is called the antecedent, and expression below the line is called the conclusion. A rule with no antecedent is an axiom.
The variable
For example
Also present in these derivations may be a typing context or typing
environment written as
Here is an example for a typing rule for addition using contexts:
In the case where the property is always implied regardless of the context we will shorten the expression. This is just a lexical convention.
In the context of modeling the semantics of programming languages using this logical notation, we often refer to two fundamental categories of rules of the semantics.
- Statics : Semantic descriptions which are derived from the syntax of the language.
- Dynamics : Semantics descriptions which describe the value evolution resulting from a program.
Type safety is defined to be the equivalence between the statics and the dynamics of the language. This equivalence is modeled by two properties that relate the types and evaluation semantics:
- Progress : If an expression is well typed then either it is a value, or it can be further evaluated by an available evaluation rule.
-
Preservation : If an expression
$e$ has type$\tau$ , and is evaluated to$e'$ , then$e'$ has type$\tau$ .
The word "type" is quite often overload in the common programming lexicon. Other languages often refer to runtime tags present in the dynamics of the languages as "types". Some examples:
# Python
>>> type(1)
<type 'int'>
# Javascript
> typeof(1)
'number'
# Ruby
irb(main):001:0> 1.class
=> Fixnum
# Julia
julia> typeof(1)
Int64
# Clojure
user=> (type 1)
java.lang.LongWhile this is a perfectly acceptable alternative definition, we are not going to
go that route and instead restrict ourselves purely to the discussion of static
types, in other words types which are known before runtime. Under this set of
definitions many so-called dynamically typed languages often only have a
single static type. For instance in Python all static types are subsumed by the
PyObject and it is only at runtime that the tag PyTypeObject *ob_type is
discriminated on to give rise to the Python notion of "types". Again, this is not
the kind of type we will discuss. The trade-offs that these languages make is
that they often have trivial static semantics while the dynamics for the
language are often exceedingly complicated. Languages like Haskell and OCaml are
the opposite point in this design space.
Types will usually be written as
The arrow type will be the type of function expressions, the left argument being the input type and the output type on the right. The arrow type will by convention associate to the right.
In all the languages which we will implement the types present during compilation are erased. Although types are possibly present in the evaluation semantics, the runtime cannot dispatch on types of values at runtime. Types by definition only exist at compile-time in the static semantics of the language.
The real quantity we're interested in formally describing is expressions in programming languages. A programming language semantics is described by the operational semantics of the language. The operational semantics can be thought of as a description of an abstract machine which operates over the abstract terms of the programming language in the same way that a virtual machine might operate over instructions.
We use a framework called small-step semantics where a derivation shows how individual rewrites compose to produce a term, which we can evaluate to a value through a sequence of state changes. This is a framework for modeling aspects of the runtime behavior of the program before running it by describing the space of possible transitions type and terms may take. Ultimately we'd like the term to transition and terminate to a value in our language instead of becoming "stuck" as we encountered before.
Recall our little calculator language from before when we constructed our first parser:
data Expr
= Tr
| Fl
| IsZero Expr
| Succ Expr
| Pred Expr
| If Expr Expr Expr
| ZeroThe expression syntax is as follows:
The small step evaluation semantics for this little language is uniquely defined by the following 9 rules. They describe each step that an expression may take during evaluation which may or may not terminate and converge on a value.
The evaluation logic for our interpreter simply reduced an expression by the predefined evaluation rules until either it reached a normal form ( a value ) or got stuck.
nf :: Expr -> Expr
nf t = fromMaybe t (nf <$> eval1 t)
eval :: Expr -> Maybe Expr
eval t = case isVal (nf t) of
True -> Just (nf t)
False -> Nothing -- term is "stuck"Values in our language are defined to be literal numbers or booleans.
isVal :: Expr -> Bool
isVal Tr = True
isVal Fl = True
isVal t | isNum t = True
isVal _ = FalseWritten in applicative form there is a noticeable correspondence between each of the evaluation rules and our evaluation logic.
-- Evaluate a single step.
eval1 :: Expr -> Maybe Expr
eval1 expr = case expr of
Succ t -> Succ <$> (eval1 t)
Pred Zero -> Just Zero
Pred (Succ t) | isNum t -> Just t
Pred t -> Pred <$> (eval1 t)
IsZero Zero -> Just Tr
IsZero (Succ t) | isNum t -> Just Fl
IsZero t -> IsZero <$> (eval1 t)
If Tr c _ -> Just c
If Fl _ a -> Just a
If t c a -> (\t' -> If t' c a) <$> eval1 t
_ -> NothingAs we noticed before we could construct all sorts of pathological expressions that would become stuck. Looking at the evaluation rules, each of the guarded pattern matches gives us a hint of where things might "go wrong" whenever a boolean is used in the place of a number and vice versa. We'd like to statically enforce this invariant at compile-time instead, and so we'll introduce a small type system to handle the two syntactic categories of terms that exist. In addition to the arrow type, we add the abstract type of natural numbers and the type of booleans:
Which is implemented in Haskell as the following datatype:
data Type
= TBool
| TNat
| TArr Type TypeNow for the typing rules:
These rules restrict the space of all possible programs. It is more involved to show, but this system has both progress and preservation as well. If a term is now well-typed it will always evaluate to a value and cannot "go wrong" at evaluation.
To check the well-formedness of an expression we implement a piece of logic known as type checker which determines whether the term has a well-defined type in terms of typing rules, and if so returns it or fails with an exception in the case where it does not.
type Check a = Except TypeError a
data TypeError
= TypeMismatch Type Type
check :: Expr -> Either TypeError Type
check = runExcept . typeoftypeof :: Expr -> Check Type
typeof expr = case expr of
Succ a -> do
ta <- typeof a
case ta of
TNat -> return TNat
_ -> throwError $ TypeMismatch ta TNat
Pred a -> do
ta <- typeof a
case ta of
TNat -> return TNat
_ -> throwError $ TypeMismatch ta TNat
IsZero a -> do
ta <- typeof a
case ta of
TNat -> return TBool
_ -> throwError $ TypeMismatch ta TNat
If a b c -> do
ta <- typeof a
tb <- typeof b
tc <- typeof c
if ta /= TBool
then throwError $ TypeMismatch ta TBool
else
if tb /= tc
then throwError $ TypeMismatch tb tc
else return tc
Tr -> return TBool
Fl -> return TBool
Zero -> return TNat
The pathological stuck terms that we encountered previously in our untyped language are now completely inexpressive and are rejected at compile-time.
Arith> succ 0
succ 0 : Nat
Arith> succ (succ 0)
succ (succ 0) : Nat
Arith> if false then true else false
false : Bool
Arith> iszero (pred (succ (succ 0)))
false : Bool
Arith> pred (succ 0)
0 : Nat
Arith> iszero false
Type Mismatch: Bool is not Nat
Arith> if 0 then true else false
Type Mismatch: Nat is not BoolThis is good, we've made a whole class of illegal programs unrepresentable. Lets do more of this!
The simply typed lambda calculus ( STLC ) of Church and Curry is an extension of the lambda calculus that annotates each lambda binder with a type term. The STLC is explictly typed, all types are present directly on the binders and to determine the type of any variable in scope we only need to traverse to its enclosing scope.
The simplest STLC language is these three terms, however we will add numeric and boolean literal terms so that we can write meaningful examples.
We can consider a very simple type system for our language that will consist of
Int and Bool types and function types.
The typing rules are quite simple, and again we get the nice property that there is a one-to-one mapping between each syntax term and a typing rule.
- T-Var Variables are simply pulled from the context.
- T-Lam lambdas introduce a typed variable into the environment when inferring the body.
- T-App Applications of a lambda with type
t1 -> t2to a value of typet1yields a value of typet2.
The evaluation rules describe the nature by which values transition between other values and determine the runtime behavior of the program.
Since we now have the notion of scoped variables for lambda, we will implement a
typing environment Env as manifest as
type Env = [(Name, Type)]
extend :: (Name, Type) -> Env -> Env
extend xt env = xt : env
inEnv :: (Name, Type) -> Check a -> Check a
inEnv (x,t) = local (extend (x,t))
lookupVar :: Name -> Check Type
lookupVar x = do
env <- ask
case lookup x env of
Just e -> return e
Nothing -> throwError $ NotInScope xThe typechecker will be a ExceptT + Reader monad transformer stack, with
the reader holding the typing environment. There are three possible failure
modes for our simply typed lambda calculus typechecker:
- The case when we try to unify two unlike types.
- The case when we try to apply a non-function to an argument.
- The case when a variable is referred to that is not in scope.
data TypeError
= Mismatch Type Type
| NotFunction Type
| NotInScope Name
type Check = ExceptT TypeError (Reader Env)There is a direct equivalence between syntax patterns here and the equivalent typing judgement for it. This will not always be the case in general though. The implementation of the type checker is as follows:
check :: Expr -> Check Type
check expr = case expr of
Lit (LInt{}) -> return TInt
Lit (LBool{}) -> return TBool
Lam x t e -> do
rhs <- inEnv (x,t) (check e)
return (TArr t rhs)
App e1 e2 -> do
t1 <- check e1
t2 <- check e2
case t1 of
(TArr a b) | a == t2 -> return b
| otherwise -> throwError $ Mismatch t2 a
ty -> throwError $ NotFunction ty
Var x -> lookupVar xFundamentally the evaluation of the typed lambda calculus is no different than the untyped lambda calculus, nor could it be since the syntactic addition of types is purely a static construction and cannot have any manifestation at runtime by definition. The only difference is that the simply typed lambda calculus admits strictly less programs than the untyped lambda calculus.
The foundational idea in compilation of static typed languages is that a typed program can be transformed into an untyped program by erasing type information but preserving the evaluation semantics of the typed program. If our program has type safety then it can never "go wrong" at runtime.
Of course the converse is not true, programs that do not "go wrong" are not necessarily well-typed, although whether we can prove whether a non well-typed program cannot go wrong is an orthogonal issue. The game that we as statically typed language implementors play is fundamentally one of restriction: we take the space of all programs and draw a large line around the universe of discourse of programs that we are willing to consider, since these are the only programs that we can prove properties for.
Well-typed programs don't go wrong, but not every program that never goes wrong is well-typed. It's easy to exhibit programs that don't go wrong but are ill-typed in ... any ... decidable type system. Many such programs are useful, which is why dynamically-typed languages like Erlang and Lisp are justly popular.
— Simon Peyton Jones
Power always comes at a price. Using one system you can do more things. In another you can say more about the things a program can do. The fundamental art in the discipline of language design is balancing the two to find the right power-to-weight ratio.
Some examples to try:
Stlc> (\x : Int . \y : Int . y) 1 2
2
Stlc> (\x : (Int -> Int). x) (\x : Int . 1) 2
1
Stlc> (\x : Int . x) False
Couldn't match expected type 'Int' with actual type: 'Bool'Stlc> 1 2
Tried to apply to non-function type: Int
Stlc> (\x : Int . (\y : Int . x))
<<closure>>The notation introduced here will be used throughout the construction of the Haskell compiler. For reference here is a list of each of the notational conventions we will use. Some of these terms are not yet introduced.
Notation Convention
\pagebreak