Qi for the Lisp Programmer

The Qi Top Level

The Qi top level is a read-evaluate-print loop like all functional languages. When you start it up, you get this.

Unlike Lisp the quote (') is not used. Entering hello returns hello, so symbols are implicitly quoted.

Each input is numbered starting with 0. You can repeat an input by typing !<n> where <n> is a natural number. Qi will print the nth input and evaluate it. You can also repeat an input by typing !<s> where <s> is any series of symbols. Qi will print and then evaluate the last input whose main function symbol begins with <s>. % works rather like ! except that the previous input(s) are printed off without being evaluated.

Extra inputs on a line are ignored.

Functions

Functions are applied in prefix form just like Lisp. Unlike Lisp, Qi is case-sensitive, so b and B are not treated as the same. = is the general equality relation (unlike Lisp where it is used for only numbers). Unlike Lisp, Qi uses true and false as booleans. ^ breaks off input.

Currying and Partial Applications

Qi permits currying and also partial applications, which generate Lisp closures.

All Qi system functions can be curried except let, cons, @p, error, output, make-string and do.

Abstractions

In Lisp the expression (FUNCTION (LAMBDA (X) X)) does the job of the identity function. In lambda calculus, it would be written (l x x). In Qi it is written (/. X X), and evaluates to a closure.

In Common Lisp, (FUNCTION (LAMBDA (X) X)) cannot be applied to an object directly, but needs to be used in a call (e.g. using FUNCALL).

((FUNCTION (LAMBDA (X) X)) 7) gives EVAL: #'(LAMBDA (X) X) is not a function name

(FUNCALL (FUNCTION (LAMBDA (X) X)) 7) gives 7.

In Qi an abstraction can always be used in place of a function. (/. X Y (* X Y)) is an acceptable shorthand for (/. X (/. Y (* X Y))).

Lists

A list begins with a [ and ends with a ]. Spaces seperate items.

cons works as the Lisp CONS. head and tail take the CAR and CDR of a non-empty list. The infix | works as in Prolog.

Qi Functions without Variables

Suppose we have to define a function f that, if it receives 1 returns 0 and if it returns 0 returns 1. We can write this as a Lisp function.

(DEFUN f (X)
(COND ((ZEROP X) 1)
((= X 1) 0)
(T (ERROR "Input to f is not 0 or 1.~%"))))

In Qi this appears as

The error condition is handled automatically.

Another example; we have a function g that returns b given a and c given b. We write this as

(DEFUN g (X)
(COND ((EQ X 'a) 'b)
((EQ X 'b) 'c)
(T (ERROR "Input to g is not a or b.~%"))))

In Qi .....

Qi Functions with Variables

Now lets look at an example using variables. We define a function factorial in Lisp

(DEFUN factorial (N) (IF (ZEROP N) (* N (factorial (- N 1)))))

This requires a variable which in Qi is any symbol beginning in uppercase (apart from NIL).

Here are some more examples

In Lisp	In Qi
(DEFUN half (x) (/ x 2))	(define half X -> (/ X 2))
(DEFUN square (x) (* x x))	(define square X -> (* X X))
(DEFUN cube (x) (* x (square x)))	(define cube X -> (* X (square X)))
(DEFUN average (x) (/ (total x) (LENGTH x)))	(define average X -> (/ (total X) (length X)))

Qi Functions with Patterns

Here is total in Lisp.

(DEFUN total (L)
(IF (NULL L) 0 (+ (CAR L) (total (CDR L)))))

Here is the Lisp member function (equivalent to MEMBER X Y :TEST 'EQUAL).

(DEFUN mymember (X L)
(COND ((NULL L) NIL)
((EQUAL X (CAR L)) L)
(T (mymember X (CDR L)))))

Here is a Lisp function that tries to divide a list into triples - if it cannot, it outputs an error.

(DEFUN triples
(COND ((NULL L) NIL)
((CONSP (CDDR L)) (CONS (LIST (CAR L) (CADR L) (CADDR L)) (triples (CDDDR L)))
(T (ERROR "Cannot make triples."))))

Here all these functions are in Qi. Here it is in Qi. Notice how in the definition of member, repeated variables are used to handle the (EQUAL X (CAR L)) in the Lisp definition. The underscores _ work as in Prolog and ML - they indicate that the structure in that part of the input is not of interest.

Here it is in Qi, the syntax is similar to Prolog (minus the commas).

Qi Functions with Guards

Like Miranda, Qi supports guards.

The following Lisp function takes a list of two numbers and returns the biggest or raises an error if there is no largest.

(DEFUN find_bigger (X)
(COND ((AND (LISTP X) (= (LENGTH X) 2))
(IF (> (CAR X) (CADR X)) (CAR X)
(IF (> (CADR X) (CAR X)) (CADR X)
(ERROR "find_bigger has failed.~%"))))
(T (ERROR "find_bigger has failed.~%"))))

In Qi, the function can be coded with guards.

Qi Higher Order Functions

Here is mapcar in Lisp

(DEFUN mymapcar (F L)
(IF (NULL L) NIL (CONS (FUNCALL F (CAR L)) (mymapcar F (CDR L))))

Here it is in Qi (FUNCALL is not needed).

If we type to Lisp

(mymapcar 'mymember '(1 2 3))

we get

APPLY: too few arguments given to mymember

But if we type (mymapcar mymember [1 2 3]) to Qi we get a list of partial applications.

This Lisp function takes a number and a list and multiplies each element of the list by the number.

(DEFUN *n (N L)
(MAPCAR (FUNCTION (LAMBDA (X) (* N X))) L))

Here it is in Qi, map in Qi is MAPCAR.

Loading and Commenting Code

(load "my code.txt") will load a Qi program in the file my code.txt.

\Here is a comment in Qi
it goes on and on and on

even with odd line breaks

until it meets another backslash here. \

Note the semi-colon is just another character in Qi.

Types

So far Qi looks like an untyped language (e.g. like SASL). Actually Qi does have type checking, but you have to switch it on. (tc +) does it. The + shows that you are now working in a statically typed environment. Qi will typecheck everything that is loaded or entered into the image. (tc -) switches the typechecker back off.

--> is the function space operator.

Like ML, mixed lists will not now be accepted.

(3+) [1 a]
type error

(4+) [1 2 3]
[1 2 3] : (list number)

You can trace type errors by entering (spy +).

Qi has tuples, the pair <1,"sausage"> is represented as (@p 1 "sausage") in Qi.

The functions fst and snd select the first and second elements of a pair.

Qi is like Hope in requiring explicit types to be attached to functions. It supports polymorphism.

The reason Qi uses explicit typing is that it does not require the user to create constructor functions in user defined types (see next section).

You can use @p in a pattern-directed manner in function definitions.

Defining New Types

The real innovation in Qi is the use of sequent notation to define types. This is an enormously powerful means of defining types which gives Qi capacities beyond ML or even more recent languages such as Haskell. The use of sequent notation derives from Gerhard Gentzen who developed the sequent calculus treatment of first-order logic. In Gerhard's system a sequent is a pair composed of two lists of logical formulae called the antecedent and the succeedent respectively. The sequent is valid if the conjunction of the elements of the antecedent logically implies the disjunction of the elements of the consequent. The concept of logical implication is defined by laying down a series of sequent rules that say how sequents may be proved.

If the succeedent is restricted by only allowing one element in the list, then the system is a single-conclusion sequent calculus system; which is the kind that Qi is designed to represent. Qi requires that user-defined types be defined in terms of sequent rules. In other words, to define a type in Qi is to say how objects can be proved to belong to that type.

For instance, suppose we wish to define a type binary composed of all non-empty lists of 0s and 1s. Using sequent notation we would write:

if X e {0,1}X : zero-or-one;

This says that for any X, any sequent whose conclusion is X : zero-or-one (meaning X is of the type zero-or-one) is provable if the side-condition is satisfied (namely X is an element of the set {0, 1}). In Qi we writeif

(element? X [0 1]) : zero-or-one;

We state the simplest condition for being a binary number. Next we have two rules that say how bigger binary numbers are built out of smaller ones.

X : zero-or-one;[X] : binary;

\ binary_right \X : zero-or-one; Y : binary;[X | Y] : binary;

\ binary_left \X : zero-or-one, [Y | Z] : binary >> P;[X Y | Z] : binary >> P;

This says that if we have a list of at least two elements X and Y (followed by 0 or more elements Z), which is assumed to be binary, then we can replace this assumption by the assumption that [Y | Z] is binary and X : zero-or-one. We need both rules because the first rule says how to prove conclusions of the form .... : binary and the second tells us what we can infer from assumptions of the form .... : binary.

Here is a script showing the definition of the datatype binary as a non-empty list of 1s and 0s.The function complement calculates the complement of a binary number. Notice there are no special constructor functions for binary numbers - we just use lists of zeros and ones in a natural way. But this means that there is no obvious way of telling if [1 1 1 0] is intended to be a list of binary numbers or a list of numbers. To avoid headaches and combinatorial problems in typechecking, Qi insists on the explicit typing of functions.

This approach to defining types gives greater freedom to define types than is current with mainstream functional languages. The use of sequent notation is underpinned by the powerful Qi compiler that reduces such rules to machine code. Since sequent notation is generic across many kinds of formal system, the Qi compiler can be used to support work in many aspects of automated reasoning.

Mark