Mark Tarver | 10 Jul 22:55 2010
Picon
Picon

why real time type checking would be a big help to programmers

sorry this disappeared .....

Some time on qilang - back in January I think - there was discussion
about how to do typechecking in Qi without having to have the user
type in annotation like {A --> A --> boolean} etc.   People have
written to me and asked why I did not do this. This happens in
languages like SML.  This is not feasible in the general case, though
I did not explain why.  I'm taking a short break and I'll now explain
why.

Why ML Implicit Type Checking is Not Feasible in Qi

Generally this is not feasible in a language like Qi because the T*
algorithm which drives Qi is optimised for these  annotations.  Could
we not replace T* by something which does not depend on annotations?
Yes; there is already such an algorithm.  It is the T algorithm
mentioned in FPQi.

Now FPQi does not  talk too much about the time complexities of the T*
algorithm, although it does say that the execution of T* is about 7X
faster (i.e. 7X fewer inferences) for a specific case.  Actually the
difference is more drastic than that - T executes in exponential time
wrt to the number of rules in a function because full backtracking has
to be used between rules. It gets even worse than that because if you
load a file, then *without annotations*, the object of proof is not
the rule as in  T*, or even the set of rules in a function ** but the
set of rules in the file. **

Such search spaces can be gigantic, dwarfing the capacity of even the
fastest inference engine to compute them.   Even with an (e.g.) 10 MIP
inference engine (about 30x the speed of the one in Qi II, SBCL
platform) to try to traverse this search space would be like trying to
travel to the Crab Nebula in the Space Shuttle.

Why does this not apply to ML?  For several reasons; but one important
one is the way that ML imposes a very restrictive syntax for defining
new types which forces the programmer to signal the nature of the
objects he is working with by the appropriate constructor functions.
These are effectively hand-waving signals for a type checker to avoid
getting lost.  In Qi, you are free to use a natural construction (look
at the definition of the binary type in chapter 11 of FPQi which just
uses 1s and 0s in a list) using the ubiquitous list.    But this great
freedom means that annotation is needed.

Real Time Type Checking = Less Annotation

A better solution than yearning for the impossible is *real time type
checking* in which, though the user types annotations, the type
checker works in real time as he types to annotate his *unwritten*
program ahead of him and corrects his errors as he works.   The idea
is simple though the details not easy to implement.

Example:   I begin to type a function that works on wffs in Qi

(define do-hairy-stuff
   {wff --> wff}
   [P & Q] -> [(process_conj P) & (process_conj Q)]
    ............

At this point the computer writes out for me in red

(define process_conj
   {wff --> wff}
   ...........

You can divine from the structure of the function that process_conj
must have the type wff --> wff and you can get the computer to share
this insight by adding process_conj : A as a premiss to the
deduction.  The computer will draw off the binding A to  'wff --> wff'
by unification.

It's not to hard to see that this will work and how but it does
require an editor which can integrate functional programming with
editing.

Mark

--

-- 
You received this message because you are subscribed to the Google Groups "Qilang" group.
To post to this group, send email to qilang@...
To unsubscribe from this group, send email to qilang+unsubscribe@...
For more options, visit this group at http://groups.google.com/group/qilang?hl=en.


Gmane