Hi,
I hope I'll not spam the list, but I wanted to show off a simple example of
the type checking done
for guile. It follows typed racked features. What's missing is the
possibility to typecheck
e.g. map with arbitrary many arguments. But recursive types are in and seems
to work.
What needs to go in is a better handling of lambdas, and the possibility to
declare functions
with arbitrary many arguments like in typed racket. Keyword arguments needs
to work as well.
/stefan
;; Example of typechecking
;;if this is #t a trace of the type deduction is shown
(set! *type-trace* #f)
#|
Type system symbols
|#
(set! *type-symbols*
'(lambda arg
or and not
cons tree1 tree2 list list2 nil
rec up down void
string symbol char boolean
number integer))
#|
this is used as such in
Assume X : (or string symbol)
for:
(if (string? X) A B)
X will be forced to be of type string in A
|#
(set! *predtypes*
`((string? ,(lambda () 'string ))
(symbol? ,(lambda () 'symbol ))
(integer? ,(lambda () 'integer ))
(number? ,(lambda () 'number ))
(boolean? ,(lambda () 'boolean ))
(pair? ,(lambda () `(cons ,(gensym "A") ,(gensym "B"))))
(char? ,(lambda () 'char ))))
;;declaring type signatures for some common lambdas
(declare + : (lambda (number number) number))
(declare - : (lambda (number number) number))
(declare < : (lambda (number number) boolean))
(declare cons : (lambda (A B) (cons A B)))
(declare car : (lambda ((cons A B)) A))
(declare cdr : (lambda ((cons A B)) B))
(declare pair? : (lambda (A) boolean))
;;subtype declaration
(subtype integer is-a number)
;;tree recursive types
(define-recursive-type (tree1 A)
(or (and A (not (cons B C)))
(cons (tree1 A) (tree1 A))))
;; An alternative because A => (cons (tree A) (tree A))
;; we can use the alternative
(define-recursive-type (tree2 A)
(or (cons (tree2 A) (tree2 A))
A))
;; list like types follows similarly
(define-recursive-type (list A)
(or nil (cons A (list A))))
(define-recursive-type (list2 A B)
(or (cons A (list2 A B))
B))
#|
subtype example
|#
#|
(define (twice X) (+ X X))
|#
(tdefine (twice X)
(type (lambda (integer) number)
(+ X X)))
#|
recursive tree examples
|#
(tdefine (rec1 X)
(type (lambda ((tree1 char)) (tree1 char))
(if (pair? X)
(let ((Car (car X)))
(if (pair? Car)
(car Car)
Car))
X)))
(tdefine (rec2 X)
(type (lambda ((tree1 A)) (tree1 A))
(if (pair? X)
(let ((Car (car X)))
(if (pair? Car)
(car Car)
Car))
X)))
(tdefine (rec2 X)
(type (lambda ((tree2 A)) (tree2 A))
(if (pair? X)
(let ((Car (car X)))
(if (pair? Car)
(car Car)
Car))
X)))
(tdefine (rec3 X)
(type (lambda ((tree2 A)) (tree2 A))
(if (pair? X)
(let ((Car (car X)))
(if (pair? Car)
(rec2 (car Car))
(rec2 Car)))
(rec2 X))))
;; Trying to compare infinite sequence types
(define-recursive-type (up A B)
(or (cons A (up A B))
(cons B (up A B))))
(define-recursive-type (down A B)
(cons A (cons A (down B A))))
;; this will typecheck without a diving into an infinite loop
;; e.g. X : (down char number) unified with (up char number)
(tdefine (down/up1 X)
(type (lambda ((down char number)) (up char number))
X))
;; similarly
(tdefine (down/up2 X)
(type (lambda ((down A B)) (up A B))
X))
;; look this does not typecheck wich shows that it works if
;; a type error is signaled
;; note X produces (down A B) which is more general production then allowed
;; by the func spec (up A A)
(catch
#t
(lambda ()
(tdefine (down/up3 X)
(type (lambda ((down A B)) (up A A))
X)))
(lambda x
(format #t "OK, if this is a type error~%")))
;; A case lambda example
(tdefine a-car
(case-lambda
((A) (type (lambda ((list number)) number)
(if (pair? A)
(car A)
0)))
((A B) (type (lambda ((list number) number) number)
(if (pair? A)
(car A)
B)))))
(tdefine (car10 X)
(type (lambda ((list number)) number)
(a-car X 10)))
;; A letrec example
(tdefine (my-map F L)
(type (lambda ((lambda (arg A) B) (list A)) (list B))
(letrec ((H (lambda (L)
(type (lambda ((list A)) (list B))
(if (pair? L)
(cons (F (car L)) (H (cdr L)))
'())))))
(H L))))
(tdefine (double-it L)
(type (lambda ((list number)) (list number))
(my-map (lambda (X)
(type (lambda (number) number)
(+ X X)))
L)))
;; A little more complex letrec example
(tdefine (oddeven N)
(type (lambda (number) number)
(letrec ((Odd (lambda (N M)
(type (lambda (number number) number)
(Even (- N 1) M))))
(Even (lambda (N M)
(type (lambda (number number) number)
(if (< N 0)
M
(Odd (- N 1) (+ M 1)))))))
(Even N 0))))
;buggy and by design set! sematics are weak but it's possible
;to use multiple types although it's a fragile construction so
;try to avoid using this and keep a single type for a variable
(tdefine (myset X Y)
(type (lambda (number symbol) symbol)
(let ((A (type (or number symbol)
1)))
(set! A (+ X 1))
(set! A Y)
'ok)))
