A hindley-milner typechecker with inductive types.
Go to file
2022-05-03 22:16:46 +02:00
app able to typecheck files ! 2022-01-28 20:50:02 +01:00
src fixed loop in anti loop detection 2022-03-01 18:10:18 +01:00
.gitignore added some build stuff 2022-01-23 12:52:33 +01:00
bad.hm added positivity check 2022-01-31 16:14:47 +01:00
hm.cabal able to typecheck files ! 2022-01-28 20:50:02 +01:00
hm.cf hm.cf: remove redundant comment 2022-01-29 00:13:01 +01:00
LICENSE added some build stuff 2022-01-23 12:52:33 +01:00
readme.md update readme a bit 2022-05-03 22:16:46 +02:00
Setup.hs only rebuild grammar when source has been modified 2022-01-23 13:58:15 +01:00
test.hm fixed loop in anti loop detection 2022-03-01 18:10:18 +01:00
TODO it can now infer the type of some expressions 2022-01-25 21:00:12 +01:00

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.