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
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
isn't available for the current version of PLT Scheme, & its replacement, MrFlow?
, isn't finished yet.
View edit of October 4, 2006
or FindPage with title or text search