Typetool

Typetool [1] is a web application developed at the University of Porto - Department of Computer Science and LIACC for the visualization of type derivation trees.
The application works for the Simple Type System [2,3] for the lambda-calculus and for the Damas-Milner Type System [4] for pure ML.
The Simple Type System is the basis of every type system for the lambda-calculus.
The Damas-Milner Type System is the basis of polymorphic systems for functional programming languages such as ML or Haskell.

Implementation

The implementation was made in Prolog and CHR along the lines presented in the paper Type Inference using Constraint Handling Rules [5].

Type Systems

The Simple Type System parser accepts lambda terms following the Haskell syntax:
The Damas-Milner Type System parser accepts lambda terms with the same syntax and some programming language constructs such as integers, booleans, conditionals and a fixpoint operator, Y:
For the Damas-Milner Type System, the types of free variables must be declared (one per line) as initial assumptions, before the term. An assumption follows the syntax:

Input
You can choose a file for input or enter a term for which to infer a principal type in the following text area: Alternatively, you may choose an example from the following set: Which type system would you like to use?

Other visualization tools and systems

References

  1. H. Simões, M. Florido. TypeTool - A Type Inference Visualization Tool. In Proceedings of the 13th International Workshop on Functional and (Constraint) Logic Programming, Aachen, Germany, June, 2004.
  2. H. B. Curry. Functionality in Combinatory Logic. In Proc. Nat. Acad. Sci. U.S.A, volume 20, pages 584-590, 1934.
  3. J. R. Hindley. Basic Simple Type Theory. In Cambridge Tracts in Theoretical Computer Science 42, Cambridge University Press, 1997.
  4. L. Damas and R. Milner. Principal Type-Schemes for Functional Programs. In Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico, pages 207-212, 1982.
  5. Sandra Alves and Mário Florido. Type Inference using Constraint Handling Rules. In International Workshop on Functional and (Constraint) Logic Programming, Kiel, Germany, ENTCS, vol.64, 2001.
Any comments and contributions are welcome. (If you are interested, please contact Hugo Simões)