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 <cleme...@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 > >
____________________ Racket Users list: http://lists.racket-lang.org/users
