Typechecking I

[Stefan Israelsson Tampe]

Hi,

Ok, here is a first step to analyse code.

Note,
attached to the mail is a modul /put it at a suitable place and fixup the
reference for the module. Then use e.g. (check '(if 1 1 1)) and you will get 
the output you see further down in the email.

We will assume that local variables in the following is gensymed to be unique
and no name clashes apear.

For typechecking i find it interesting to consider an equational approach
first. e.g. translate code to an equation system.

let's take a first simple step here and and assume that the typecheck function
just finds the equation we need to solve in order to understand type
consistency and discovery. we will assume that typecheck is of the form
(typecheck Eq Code Type) or in short
Eq     is current equational state, 
Code   the code to draw equations out of.
Type   the type associated with the result of Code

******************* Item I *******************************
[let X Y Z] : T

Translates to
(typecheck (typecheck Eq Y X) Z T)

Example of equation generation:
(let x 1 x):
((= integer x) (= x Texp))

(let x 1 (let y x y)):
((= integer x) (= x y) (= y Texp))

TODO: Note: (= y x) should be more nicer for the understanding!!!

This is not earthshaken. But I think it is wise to handle first such an 
translational step in order to write a solver in kanren or prolog or racklog
or guilelog :-) for the more general case.

******************* Item II ***************************
[begin x ... xx] : T

(typecheck x e) o ... o (typecheck xx T)

the symbol e will mean an anything object so that essentially [= e x] is true 
for all x. You could say everything that we have not assigned a type to has
type e and then (the idea) is that the all scheme expression should
typecheck. It remains to define the properties and rules associated with e to
make this work. The target is to be able to gradually mix typed expressions
with untyped expression.

Example:
(begin 1 "a" 1):
((= integer  e) 
 (= string   e) 
 (= integer  Texp))

******************* Item III ****************************
[lambda [x ...] code]

What to look up for here is that essentialle every usage of a lambda inside
a function has to, to be general, have a unique set of equations and do a 
unique deduction. This can be expensive, but is the correct way to treat the 
typechecking of the lambda. So we must tell the solver later on that we are 
going to treat a lambda, e.g. x ... will be a unique version at every usage
of the lambda the directive for the solver is (lambda vars res equation)
lambda conceptually translates to an abstraction of an equations.

Example
(lambda (x y) x):
((= (lambda (x y) Tlam6583 
       ((= x Tlam6583))) Texp))

********************** Item IV **************************
[apply f [x ...]] : T

First of all we need to deduce the equation of f, to yield a lambda. e.g.
(typecheck f [lamda [ArgType(x) ...] ResType]) o
(typecheck x [arg ArgType(x)]                ) o ... o
(add-equation [= [res ResType] T])

so
1. define the functional signatur.
2. find the equations typececked to [arg X], arg is a directive to the solver
   to tell it that we are equating a function argument why? well the equality
   needs to be treated differnetly in order to be correct.
3. the same reason for the addition of the last equation. we need to inform 
the
   solver that ResType is of a result type.

Example:
(apply (lambda (x y) x) (1 2)) :
((= (lambda (x y) Tlam6954 ((= x Tlam6954)))   ;; a lambda type abstraction 
    (lambda (Targ6951 Targ6952) Tres6953))     ;; a lambda type
 (= integer (arg Targ6951))
 (= integer (arg Targ6952))
 (= (res Tres6953) Texp))


Can you see how res and arg differ
(= T (arg (or A B C)))   ; argument can be A or B or C
(= T (res (or A B C)))   ; function produces A or B or C

**************** Item V *************
[if P X Y] : T

(integer? X) makes a promise that if true then X is an integer and
is a string. Consider (= (res A) (arg integer)) if the result of a function
is anything it follows that it can't unify with an argument that has to 
take an inte integer as in the case
(+ (g X) 1) and g is not typehcecked and we cannot ussume anything
about it hence the typecheck should fail. On the other hand
(if (integer? (g X)) (+ (g X) 1) #f) should be able to typecheck
against (or integer boolean) and here we would have an equality of the
type (= (validated integer) (res A)) and then A=integer in the rest of the
equations in the or.

Example:
(let x 1 (if (integer? x) "a" 2))
=================================
(= integer x)
 (or ((=  x (validated integer)) (= string Texp))
     ((=  x (validated (not integer)))
      (=  integer Texp))))



So maybe it's an unessesary step but at least I appriciate this little 
transformation to get an understanding the subject. I'll will now work
a little with solving the equations. 

And yes, all tree-il is not included, but I fix the complexity at this level
and move over to solving the equations.

Play around and have fun
/Stefan

equationalize.scm
Description: Text Data