[racket] Reading recommendation for static analysis?

On Jan 2, 2012, at 6:40 PM, Patrick Li wrote:

> Hello everyone,
> 
> I am trying to accomplish the following task, and was wondering if anyone knows of a fitting paper that I can read. I want to write a static analysis tool for a small scheme-like language to catch simple typing errors. The following is a simple example of the type of errors that I would like to detect:
> 
> 1) let b = (or (pair? x) (string? x))  ;; compute whether x is a pair or a string
> 2) assert b   ;; early exit the program if b is false.
> 3) result = x * 2 ;; <--- This is a type error that can be found using static analysis.
> 
> In words, the pseudocode fragment says:
> 1) Let b be a boolean, it indicates whether x is a pair or string.
> 2) Assert that b must be true.
> 3) Store x times 2 into result. This must be a type error because, for program execution to reach this point, x must either be a pair or a string, otherwise the assertion would have failed. Therefore, since x is either a pair or a string, it is definitely not an integer.

It looks to me like this is exactly the problem that "occurrence typing" solves, and that typed racket implements.  To wit:

#lang typed/racket

(: my-fun (Any -> Any))
(define (my-fun x)
  (cond [(not (or (string? x) (pair? x)))
         (error 'my-fun "oh dear, I wanted a string or a pair")]
        [else (* x 2)]))

=>

Type Checker: Expected Complex, but got (U String (Pairof Any Any)) in: x


John

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4624 bytes
Desc: not available
URL: <http://lists.racket-lang.org/users/archive/attachments/20120103/c5aa617d/attachment.p7s>