|I have started this
occasional series on type theory in Qi for the benefit of people who are interested in
exploring the further ranges of type theory, which are
beyond the easy reach of less powerful systems like ML
and Haskell. Several bolder spirits of this kind have
written to me asking about whether Qi can be used to type check
Lisp code. Generally the answer is 'yes'. Qi is good for
experimenting with type systems. I put this short page
together to help those of you who wanted to learn more.
A long time ago in America I believe you had
what were called 10 cent stores where you could get basic
articles very cheaply. I guess today 10 cents does not go
very far, but in the spirit of these vanished icons of
American culture, I offer you a 10 cent Lisp type
checker. A very basic model that you can tweak and
improve on for your own learning.
Tiny Lisp is a species of Lisp that I've used to teach
computability. It is Turing complete, but remarkably
small. It uses the following set
cons, car, cdr, if, equal, 1+, 1-
What we will do here is create a type
checker for Tiny Lisp in Qi . All ready? Ok, here goes.
First of all there is some tiresome stuff to do with
case. Qi is
case sensitive and all inbuilt Lisp functions are in
uppercase. Also Qi variables, like Prolog
variables, begin in uppercase. To avoid confusion, we
work in lower case when mentioning Lisp functions. This
means that we need to define our own 'defun', 'car' etc.
This is no big deal. Here is the Lisp.
defun (f params code) `(DEFUN ,f ,params ,code))
(DEFUN car (x) (CAR x))
(DEFUN cdr (x) (CDR x))
(DEFUN equal (x y) (EQUAL x y))
Second problem is that lowercase 'if'
and 'cons' exist in the Qi system already. Qi has proper booleans, unlike Lisp which doubles
NIL as the boolean false and as the empty list. To avoid
confusion we use our own versions.
tee! () T)
(DEFUN empty! () NIL)
(DEFUN lispcons (x y) (CONS x y))
(DEFMACRO lispif (x y z) `(IF ,x ,y ,z))
So instead of T we write (tee!) and
instead of NIL we write (empty!). Its easy to set up
'defun' so that these replacements are made by the
computer. I leave that change to you.
What is a Symbol?
Another challenge we will face is that we will be working
with formal parameters like 'x' and 'y' and we will want
to know what their type is. Qi recognises such objects as having the type
'symbol' which is not helpful to us. These formal
parameters are place holders and the fact we are using
symbols as place holders does not mean that every formal
parameter has the type 'symbol'. In Qi , any symbol prefixed by && is treated
as a place holder. So we will use Qi placeholders to stand for objects of an unknown
We're going to make some simplifying assumptions about
Tiny Lisp which makes it different from the real thing.
First we are going to assume it abides by the lambda
does and Lisp does not, so this is not correct, but it
makes a first attempt easier. Second, we will first deal
with only 1 place functions.
These assumptions can all be relaxed.
The Type Theory of Tiny Lisp
A Tiny Lisp function definition has
the form (defun F
(X1 ....Xn) Body). The uppercase parts are variables. The basic
rule for type checking a 1-place function is
F : (A --> B), X : A
>> Body : B;
(defun F (X) Body) : (A --> B);
There is a proviso though
- the X is a placeholder and needs to be treated as such.
Here is the revised definition using place holders.
let X* (gensym
let Body* (subst X* X Body)
F : (A --> B), X* : A >>
Body* : B;
(defun F (X) Body) : (A --> B);
We could define a general rule for
functions of any arity, but again we will keep it simple
to begin with.
The next rule is the Rule of Applications from typed
(A --> B); X : A;
(F X) : B;
The other rules give the types of Tiny
Lisp system functions. [A] is shorthand for (list A).
lispif : (bool --> (A --> (A
equal : (A --> (A --> bool));
lispcons : (A --> ([A] -->
car : ([A] --> A);
cdr : ([A] --> [A]);
if (element? F [1+ 1-])
F : (number --> number);
(tee!) : bool;
(empty!) : [A];
(empty!) : bool;
and thats it!
curries all functions except a select few which are
special - like define and let and so forth. Do we want to curry defun? Not
really - so we tell Qi to leave defun alone.
does the trick.
Testing the Checker
But does our system work? Lets try it.
TinyTypes.txt contains all the Qi code for defining the type theory of Tiny Lisp
and TinyLisp.txt contains the Lisp, so you can repeat the
following script for yourself. Type LOAD to
load the Lisp file and load to load the Qi code. We begin by
LOADing our Lisp stuff - note we use uppercase to revert
to the Lisp loader.
Off we go. We put some test cases into
a text file called TinyLispFunctions.txt.
Here is what is in the file.
(defun plus (x y)
(lispif (equal x 0) y (plus (1- x) (1+ y))))
(defun member (x y)
(lispif (equal y (empty!)) (empty!) (lispif (equal x
(car y)) y (member x (cdr y)))))
(defun join (x y)
(lispif (equal x (empty!)) y (lispcons (car x) (join
(cdr x) y))))
We load TinyLispFunctions.txt.
But if we type in (member 1 [1 2 3]) to the type checker we get a type error? Why?
Well Qi has simply not recorded its conclusions. Why
should it - since defun is just another function to Qi like + or -?
What about quotes? Quotes are tricky -
in fact our little type checker does not understand
quoting/unquoting at all. Well here is a beginning.
if (symbol? X)
(quote X) : symbol;
quote (x) `(QUOTE ,x))
This allows us to quote symbols. What
about lists? Can we say
(quote X) : A;
No. It works for 'a, but '(1+ 4) is
not a number but a list.
We can handle quoted lists by defining quote so
that it automatically places any list in cons form. Thus '(a b)
would appear as (lispcons
(quote a) (lispcons (quote b) (empty!))). This is a fairly basic exercise and I leave it
to you. Try checking
(x) (lispcons x (lispcons (quote a) (empty!))))
quoting and unquoting has some
unexpected depths - I'll leave you to the pot holing!
Functions of Any Arity
Our type checker only handles 1 place
functions, but we type checked 2-place functions. How? By
currying. We write two rules; one converts a defun into
a curried lambda function. The other tells us how to type
check lambda functions. Now we can handle any arity >=
(mk_lambda Xs Body)
F : A >> Lambda : A;
(defun F Xs Body) : A;
let X* (gensym "&&x")
let Y* (subst X* X Y)
X* : A >> Y* : B;
(lambda (X) Y) : (A --> B);
[X] Body -> [lambda [X] Body]
[X | Y] Body -> [lambda [X] (mk_lambda Y Body)])
(DEFMACRO lambda (x
y) `(FUNCTION (LAMBDA ,x ,y)))
Thus (defun foo (x y)
y) becomes (lambda (x) (lambda (y) y)).
Scaling Up to Lisp As It Is
This is a good demo of the power of Qi as a fast prototyping language (TinyTypes.txt and TinyLisp.txt total 64
lines). But what do you need to add to Tiny Lisp to make
a viable type checker for Common Lisp? Apart from
niggles, something like this:
1. Storage so that the system remembers types instead of
2. Several hundred types for system functions - like
3. Provision for polyadic functions.
4. Provision for not recognising currying - i.e.
non-lambda calculus consistency.
Some of these items are not trivial.
Type checking CL is big project; for myself I prefer to
work mainly in Qi, thus avoiding quotes and enjoying
pattern-matching. I only use Lisp for macros and odd
pieces of code. But if you want to experiment, the
beginnings are on this page. Of course you are not
limited to Lisp as your object language, you can build
type checkers for anything you want.
Copyright (c) 2005,