Mr Spidey

MrSpidey is a static type checker for DrScheme that uses set-based analysis to infer types for DrScheme programs. It implements SoftTyping, i.e. it will try to prove the program type-correct and notify the programmer when it finds constructs that are guaranteed to be wrong or that are questionable. However, it will not reject programs merely because it cannot prove them type-correct. It is claimed that this gives some of the advantages of a StaticallyTyped language, while retaining the flexibility of a DynamicallyTyped language.

http://www.plt-scheme.org/software/mrspidey/

http://download.plt-scheme.org/doc/103p1/html/mrspidey/

Could someone give us a brief explanation of how this compares with the HindleyMilnerTypeInference system as implemented in HaskellLanguage or ObjectiveCaml? - thanks

It uses PartialEvaluation based on sets of values. You can view this as a TypeInference algorithm for a more expressive type system than the systems that can be handled by Hindley-Milner. Also the inference never fails, it just adds dynamic checks as necessary.

For more detail, see the paper "Set-Based Analysis for Full Scheme and Its Use in Soft-Typing" by Flanagan and Felleisen, available from http://www.cs.rice.edu/CS/PLT/Publications/Scheme/ (or the other papers listed at http://download.plt-scheme.org/doc/103p1/html/mrspidey/node26.htm).

Unfortunately, MrSpidey isn't available for the current version of PLT Scheme, & its replacement, MrFlow?, isn't finished yet.

CategoryScheme