Studies in Qi

The 10 cent Lisp Type Checker

Issue #2 in Advanced Type Theory

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

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

defun, 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.

(DEFMACRO 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.

(DEFUN 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 type.

Simplifying Assumptions

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 calculus. Qi 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 (X₁ ....X_n) 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 "&&x")
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 lambda calculus.

F : (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 --> A)));

______________________
equal : (A --> (A --> bool));

___________________________
lispcons : (A --> ([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!

Specialisation

Qi automatically 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.

(specialise defun)

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 -?

Quotes

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;

(DEFMACRO quote (x) `(QUOTE ,x))

This allows us to quote symbols. What about lists? Can we say

X : A_______
(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

(defun cons_symbol (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 >= 1.

let Lambda (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);

(define mk_lambda
[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 suffering amnesia.
2. Several hundred types for system functions - like EVAL.
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.

Have fun.