[racket] Reading recommendation for static analysis?

That is brilliant. And basically exactly what I am looking for. Thank you
John!
 -Patrick

On Tue, Jan 3, 2012 at 7:52 PM, John Clements <clements at brinckerhoff.org>wrote:

>
> 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 --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20120103/96fa8ddb/attachment.html>