5 ms·
Isn't Idris basically Haskell with DT?
by HKH2 2y ago
Isn't Idris basically Haskell with DT?
- wk_end 2y agoAt the language level...sort of? Idris is strict, unlike Haskell. As of Idris 2, it also has a substructural type system which tracks how often terms are used, which is kind of Rust-y and can allow for better runtime performance by ensuring that proofs can be erased (IIUC). But besides just being a language, Haskell is a whole ecosystem. It's not an amazing ecosystem, but it's good enough for serious work. Idris is not and may never be. A fully-supported Dependent Haskell would be huge for dependent types in practice.
- jech 2y ago> Idris is strict, unlike Haskell. "The next Haskell will be strict." — Simon Peyton-Jones