A Calculus for Constraint-Based Flow Typing

Provided by: Victoria University Topic: Software Date Added: Mar 2012 Format: PDF
Flow typing offers an alternative to the traditional Hindley-Milner approach to type inference. A key distinction is that variables may have different types at different program points. Flow typing systems are typically formalised in the style of a dataflow analysis. Whilst a natural choice, this can hinder the formalisation and lead to difficult questions about termination. The authors present an alternative constraint-based formalisation of flow typing which leads to a simple proof of termination. Type inference is useful for simplifying and reasoning about statically typed languages. Scala, OCaml and, most recently, Java 7 all employ local type inference (in some form) to reduce syntactic overhead. Type inference can also be used to type existing untyped programs (e.g. in JavaScript or Python).

Find By Topic