3 ms·

Or Idris, which is (IMO) more practically useful than Agda.

• chowells 11y ago
  The 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.