Although LISP doesn't use static type checking, it's instructive to introduce a few type checking rules. We call LISP with type checking LISP++.
We can use formation axioms to declare primitive types:
int:Type
double:Type
Boolean:Type
char:Type
We can also introduce special constants and functions using axioms and rules:
0:int
n:int
n+1:int
true:Boolean
false:Boolean
The LISP language allows users to form pairs of values using the cons operation. The first and second member of a pair can be extracted using the car and cdr operations, respectively.
The formation rule says that if A and B are types, then AxB is the type of all pairs with first component from A and second component from B:
A:Type, B:Type
AxB:Type
The elimination rules says that if p is a pair of type AxB, then (car p) and (cdr p) return values of types A and B, respectively:
p:AxB
(car a):A
p:AxB
(cdr p):B
The introduction rule says that if a is of type A and b is of type B, then (cons a b) is of type AxB:
a:A, b:B
(cons a b):AxB
The computation rules show us the exact values returned by car and cdr:
p = (cons a b)
(car p) = a
p = (cons a b)
(cdr p) = b
A non-empty LISP list is simply a pair in which the second component is a list. The empty list is called null.
The formation rule says that if A is a type, then [A] is the type of all lists with members from A:
A:Type
[A]:Type
The elimination rules say that the car of a list is an element of A, while the cdr of a list is another list with members from A:
l:[A]
(car l):A
l:[A]
(cdr l):[A]
The introduction rule says that if t (for tail) is already a list of elements from A, and if h (for head) is an element of A, then (cons h t) is a new list of A elements:
h:A, t:[A]
(cons h t):[A]
In addition, we have an introduction axiom that says that null is a list:
null:[A]
The computation rules say that the car of the list (cons h t) is actually h and the tail is t:
l = (cons h t)
(car l) = h
l = (cons h t)
(cdr l) = t
By introducing a special error value that belongs to all types, we can use computational axioms to say that the empty list has neither a head nor a tail:
(car null) = error
(cdr null) = error
The function formation rule for LISP++ functions says that
if A and B are types, then
A->B is the type of all functions with domain A and range B:
A:Type, B:Type
A->B:Type
Sometimes the conclusion or assumption of a rule can be a conditional statement. We use the notation:
p=>q
to indicate that statement p implies statement q. Using this notation we can express the introduction rule as follows:
x:A => b:B
(lambda(x:A) b):A->B
For historical reasons LISP uses the lambda operator to create functions. Our variation of the lambda operator requires that parameters be typed.
The LISP syntax for calling a function is (f a) where f is a function and a is its argument. We can express this with an elimination rule:
a:A, f:A->B
(f a):B
The computation rule says that calling f is the equivalent of substituting the argument for the parameter in the body of the function. We use the notation b[x/c] to indicate this substitution:
f = (lambda(x:A) b), c:A
(f c) = b[x/c]
If A is a type, then let <A> denote the type of all variables containing values of type A. Let val be the dereferencing operator and let var be the variable constructor. Here are the rules:
A:Type
<A>:Type
v:<A>
(val v):A
v:A
(var v):<A>
v = (var a)
(val v) = a
We can specify how to type check and compute phrases using rules. For example, the LISP conditional expression allows us to choose one of two values depending on some condition:
a:A, b:A, c:Boolean
(if c a b):A
c = true
(if c a b) = a
c = false
(if c a b) = b