Qi for the Lisp Programmer

Qi for the ML 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 ML symbols are treated as self-evaluating objects; entering hello returns hello.

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 unlike ML. Like ML, 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 lambda calculus, the identity function would be written (l x x). In ML it is written (fn x => x). In Qi it is written (/. X X), and evaluates to a closure.

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 ]. In Qi spaces are used instead of commas to seperate items.

cons works as the ML ::. head and tail are equivalent to ML's hd and tl. The infix | works as in Prolog. Note that without type checking, you can have mixed lists (unlike ML). With type checking switched on (see later) this is not true.

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 an ML function.

fun f 0 = 1
| f 1 = 0;
val f = fn : int -> int
- f 1;
val it = 0 : int
- f 0;
val it = 1 : int
- f 2;

uncaught exception nonexhaustive match failure
raised at: stdIn:41.9

In Qi it is defined like this

The error condition is handled automatically.

Another example; we have a function g that returns b given a and c given b. In ML we would probably use strings unless we want to declare a new type

fun g "a" = "b"
| g "c" = "d";

in Qi, we can use symbols.

Qi Functions with Variables

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

fun factorial n =
if n = 0 then 1 else n * factorial(n - 1);

This requires a variable which in Qi is any symbol beginning in uppercase (apart from NIL which is an alternative representation of the empty list and T which is used in Lisp).

Here are some more examples

In ML	In Qi
fun half x = x div 2;	(define half X -> (/ X 2))
fun square x = x * x;	(define square X -> (* X X))
fun cube x = x * square(x);	(define cube X -> (* X (square X)))

IN ML, half has the type int -> int. In Qi, all numbers are grouped under the type number which allows half to be used on floating point numbers etc.

Qi Functions with Patterns

Here is total in ML..

fun total [] = 0
| total (x :: y) = x + total(y);

Here is the Lisp member function in ML

fun mymember _ [] = []
| mymember x (y :: z) = if x = y then (y :: z) else mymember x z;

Here is an ML function that tries to divide a list into triples.

fun triples [] = []
| triples (w :: x :: y :: z) = ([w,x,y] :: triples z);

Here all these functions are in Qi. Here it is in Qi. Notice how in the defintion of member, repeated variables are used to handle the equality in the definition of mymember. 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 ML function takes a list of two numbers and returns the biggest or raises an error if there is no largest.

exception equal;
fun find_bigger [x,y] = if x > y then x else if y > x then y else raise equal;

In Qi, the function can be coded with guards.

Qi Higher Order Functions

Here is map in ML

fun mymap _ [] = []
| mymap f (x :: y) = (f(x) :: map f y);

Here it is in Qi.

If we type to ML

- mymap mymember [1,2,3];
val it = [fn,fn,fn] : (int list -> int list) list

we get an list of functions. If we type (mymap mymember [1 2 3]) to Qi we also get a list of functions.

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

fun multn n l = map (fn x => x * n) l;

Here it is in Qi.

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. \

Types

So far Qi looks like an untyped version of ML with a different syntax (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. The triple (1,2,3) of type int * int * int in ML is represented in Qi as (@p (@p 1 2) 3) or (@p 1 (@p 2 3)). Note that these are different objects in Qi with different types (think <<1,2>, 3> and <1, <2,3>> in set theory). The functions fst and snd select the first and second elements of a pair. Qi accepts (@p 1 2 3) as a legitimate substitute for (@p 1 (@p 2 3)).

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 write

if (element? X [0 1]) : zero-or-one;X : 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.

In ML you begin by defining zero-or-one as an enumeration type and continue by defining binary as a recursive type using constructor functions.

datatype zero_or_one = zero | one;

datatype empty = e;

datatype binary = place of zero_or_one * empty | bld of zero_or_one * binary;

fun complement (place(one, e)) = place(zero, e)
| complement (place(zero, e)) = place(one, e)
| complement (bld (one, Binary)) = bld(zero, complement Binary)
| complement (bld (zero, Binary)) = bld(one, complement Binary);

Writing out [0 1 0 1] is left as an exercise.

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.

Where to Go From Here

That's the end of the 15 minute introduction. You now have enough to write Qi programs.

Mark