That is brilliant. And basically exactly what I am looking for. Thank you John!<div> -Patrick <div class="gmail_quote">On Tue, Jan 3, 2012 at 7:52 PM, John Clements <<a href="mailto:clements@brinckerhoff.org">clements@brinckerhoff.org</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im"> 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. </div>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 </blockquote></div> </div>