This was originally posted to the functional programming news group. It
contains an analysis of a form of EVAL which Lisp programmers know very
well and you might find it interesting. There is a gentle challenge to
Haskell/ML people in the post which, so far, has not been taken up
Mark
_________________________________________________________________
Original Post
I got this post reply to my Qi 6.1 announcement from Vincenzo Ciancia
"I have looked at the webpage, and found the typing system of Qi
interesting,
but I can't really grasp the difference between ocaml types, haskell
types
with type classes and sequent-calculus based types. Are the latter more
fine-grained? Can you show some simple example where the
sequent-calculus
discipline is more expressive, more powerful or in other ways "better"
than
haskell and ocaml types?"
It seems several other people are in the same boat, so I thought I'd
try to address
the question through the type of example Vincenzo requests.
I'm not going to argue that sequent calculus is 'better' than ML or
Haskell because
its not a scientifically verifiable statement. But I can give a
flavour of the approach
by example and let you judge according to your needs. Maybe
MLers/Haskellers could
show that they too have an elegant way of coping with this example.
Many years ago when I was new to ML, having moved from Lisp, I met Mike
Foreman
at the LFCS. I asked him about the EVAL function which is in Lisp and
he told me
that it was absent from ML "What is the type of EVAL?" he said. There
seemed to
be no good answer to this.
Now actually, the thrust of his question is right. There is no *type*
for EVAL, but there
is a *theory* of EVAL.
EVAL is in Qi, but its called 'eval' (wow!). Its semantics is very
simple. In Qi lists are
put together with [ ...]s. So [0 1 2] is a list composed of three
numbers. Function
applications are done with (...)s; so (+ 7 8) is 15. The semantics of
'eval' is that the
normal form of (eval E) is the normal form of E*, where E* results from
E by replacing all
the [ ...]s in E by (...)s. Here is an example script.
\(0-) is just a Qi line prompt\
(0-) [+ 1 2]
[+ 1 2]
(1-) (eval [+ 1 2])
3
eval in Qi is very powerful. If you look at chapter 8 in 'Functional
Programming in Qi" (FPQi)
(www.lambdassociates.org/webbook/chap8.htm) you'll see a
parser-generator built with eval.
See chapter 7, for the background on backtracking which is used in this
chapter.
But eval is not part of Qi type theory; so you cannot use it in type
secure code. Can eval
be given a type theory in Qi? Lets have a try.
Well, first lets make it simple by supposing that the inputs to eval
are all curried. Here is
a first bash.
First Attempt:
===========
(datatype evaltheory
F : (A --> B);
X : A;
______
(eval [F X]) : B;)
It looks like the Rule of Applications in the typed lambda calculus.
This works nicely on (eval [+ 1])
(3+) (tc +) \Switch on type checking\
true
(4+) (eval [+ 1])
#<CLOSURE :LAMBDA [X2] [+ X1 X2]> : (number --> number)
But bombs on
(5+) (eval [[+ 1] 2])
error: type error
Because [+ 1] is not of type (A --> B). OK, we need to recurse inside
[F X].
Second Attempt:
=============
Here I recurse inside [F X].
((eval F) (eval X)) : A;
____________________
(eval [F X]) : A;
This is fine; but what stops the recursion? The base cases must be
self-evaluating
objects like numbers, symbols and strings. So I add
X : symbol;
_________
(eval X) : symbol;
X : number;
__________
(eval X) : number;
and 2 or 3 more rules like this (I'll miss them out here).
Good enough? Nearly, what about functions? OK. Another rule.
F : (A --> B);
_________________
(eval F) : (A --> B);
Here it is altogether.
(6+) (datatype evaltheory
X : symbol;
_________
(eval X) : symbol;
X : number;
__________
(eval X) : number;
F : (A --> B);
_________________
(eval F) : (A --> B);
((eval F) (eval X)) : A;
____________________
(eval [F X]) : A;)
Can I typecheck (eval [[+ 3] 5])?
(eval [[+ 3] 5]) \Hurrah! It works.\
8 : number
Third Attempt
===========
Now I've got the hang of this. Can I get rid of the annoying need
to curry everything to 'eval'? Yes; I add an extra rule. In Qi,
like
in Prolog, | is used as an infix list constructor. The extra rule is
(eval [[F X] Y | Z]) : A;
____________________
(eval [F X Y | Z]) : A;
which curries for us. Here is the new theory
(datatype evaltheory
X : symbol;
_________
(eval X) : symbol;
X : number;
__________
(eval X) : number;
F : (A --> B);
_________________
(eval F) : (A --> B);
((eval F) (eval X)) : A;
____________________
(eval [F X]) : A;
(eval [[F X] Y | Z]) : A;
____________________
(eval [F X Y | Z]) : A;
(9+) (eval [- [+ 3 5] 2])
6 : number
Now this is OK as far as it goes. But really its not so useful because
what we really want to do is typecheck code like the stuff in chapter
8 which uses eval in metaprogramming. Can we use Qi to develop a
theory of eval for Qi functions? Well I'll stop there, because this is
a post and not a paper.
We can summarise the Qi approach in the way I tried to explain to
Vincenzo
"When we are dealing with types, we can often see that there are
certain logical properties which group around these
types and the functions that work with them. Sometimes
we can express these properties axiomatically or in
deductive form and sometimes we can see that the rules
we provide can be animated into a type checker.
What Qi does is give you the ability to say math'lly or
logically exactly what your theory is. The sequent
notation is compiled into fast code. So if you have
e.g. an idea of the type theory of eval or the type theory
of primes and composites, well you have the chance to
use it for a serious application and see it motor.
The *down* side is that Qi is a very sharp tool and you
can cut yourself. In particular you can create axiom
sets which will generate infinite regresses or ones that
collapse the type system altogether! See the end of
chapter 13 in FPQi for examples. You cannot do this in ML or
Haskell because you are denied this power."
I hope this illuminates a rather general remark.
Mark