readme.txt

This is a small but complete implementation of the HMF type system
described in the paper "HMF: simple type inference for first-class polymorphism",
available at "http://research.microsoft.com/users/daan/pubs.html"

This implementation uses IO references to implement substitution instead of using
explicit substitutions. Also, it uses ranked unification type variables to implement
efficient generalization.

Just load the prototype in GHCi as:

  > ghci Main.hs

and from the GHCi prompt, run the tests:

  *Main> testAll
  ...

or check some expressions yourself:

  *Main> check "\\x -> x"
  expr: \x -> x
  type: forall a. a -> a

  *Main> check "auto"
  expr: auto
  type: forall a. (forall b. b -> b) -> a -> a

  *Main> check "apply auto id"
  expr: apply auto id
  type: forall a. a -> a

  *Main> check "map auto ids"
  expr: map auto ids
  type: forall a. [a -> a]

or get some more help:

  *Main> help
  ...

See the test-cases in "Main.hs" for many more examples, 
and "Gamma.hs" for the standard available functions.

There are three provided variants of HMF type inference that can be selected in Main.hs:
 InferBasic   : Basic HMF type inference 
 InferRigid   : HMF extended with rigid type annotations
 InferRigidOpt: Optimized HMF with rigid annotations with a minimal number generalizations.
 InferNary    : Optimized Rigid HMF with taking all arguments into account for N-ary applications
 InferNaryProp: Optimized Rigid N-ary HMF with full type annotation propagation

Have fun,
-- Daan Leijen.


Modules:
--------------------------------------------------------------------------------------------
PPrint.hs           Pretty printer library
Types.hs            Basic definitions of terms and types
Parser.hs           Basic parser for terms and types
Subst.hs            Substitutions
Gamma.hs            Type environment: also contains standard functions like "const", or "id"
Operations.hs       Basic type operations: instantiate, skolemize etc.
Unify.hs            Unification and matching algorithm

InferBasic.hs       Basic HMF type inference  <--- start with this to learn about HMF inference!!
InferRigid.hs       HMF type inference extended with rigid type annotations
InferRigidOpt.hs    Optimized version with rigid type annotations where generalizations are minimal
InferNary.hs        Optimized Rigid HMF taking all arguments into account for N-ary applications
InferNaryProp.hs    Optimized Rigid N-ary HMF with full type annotation propagation

Main.hs             Main module