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