A Non-Standard Hindley-Milner Type Checker in Compositional Style with Free Variable Handling
This repository contains a unique type checking algorithm for the Hindley-Milner type system. Unlike standard implementations, tychk is designed to infer the types of expressions containing free variables. Also, it is implemented in a compositional style, meaning that the type of a larger expression is derived from the types of its sub-expressions, even if those sub-expressions have free variables.
- Type Checking Algorithm: The central type checking function
checkis implemented inlib/type.ml. - Algorithm Signature: The
checkfunction has the following type:This indicates that given an expression of typeExpr.t -> (ctx * t) option
Expr.t, thecheckfunction attempts to infer its type and the resulting type context. It returns an optional tuple of the inferred context (ctx) and the inferred type (t). If type checking fails, it returnsNone.
tychk/
├── lib/
│ ├── expr.ml # Definition of the expression type 't'
│ └── type.ml # Definition of types 't', contexts 'ctx', and the 'check' algorithm
├── bin/
│ └── main.ml # Main entry point for the type checker; feel free to try your own expression here
└── README.md
To use or explore tychk, you will need an OCaml development environment.
git clone <repository_url>
cd tychk
opam switch create .
eval $(opam env)
opam install . --deps-only
dune exec tychk