3 ms·
Fortunately, Liquid Haskell already exists. I wouldn't say it's production quality yet... But it's a work in progress, and achieves far more than you are requ
by chowells 11y ago
Fortunately, Liquid Haskell already exists.
I wouldn't say it's production quality yet... But it's a work in progress, and achieves far more than you are requesting here.
- eru 11y agoYou can also go with Agda for full on dependent typing.
- PeCaN 11y agoOr Idris, which is (IMO) more practically useful than Agda.
- chowells 11y agoThe big advantage to liquid types, a la liquid haskell, is that you get far more inference than you can get in full dependent typing. I still think liquid haskell is too immature (Integer is not a good theory for Int, type classes aren't handled well, etc), but the promise is fascinating if the issues get worked out.