A hindley-milner typechecker with inductive types.
app | ||
src | ||
.gitignore | ||
bad.hm | ||
hm.cabal | ||
hm.cf | ||
LICENSE | ||
readme.md | ||
Setup.hs | ||
test.hm | ||
TODO |
HM
A simple, terminating, pure, hindley milner lambda calculus with inductively defined types.
For an example of the syntax see test.hm
Building
Depends: * BNFC * GHC * Cabal
Instructions: * Run cabal build
TODO
Currently there is no kind system and as such there are no indexed datatypes. Considering my interest currenlty lies in dependently typed systems this is not likely to change any time soon.