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
smime.p7s
Description: S/MIME cryptographic signature
____________________ Racket Users list: http://lists.racket-lang.org/users
