4 ms·

Please, please don't let this be the top comment on Idris. I really want to hear from people who have experience with it in different regards. For example, wha

• catnaroek 11y ago
  1ML doesn't really unify the type and value languages. First-class modules are syntactic sugar over System F-omega, which means that the elaboration/type-checking phase of 1ML duly splits modules into type and value components, which live in separate worlds. Personally, I find 1ML's approach more pragmatic, or, at least, easier to digest for most programmers - including Haskell programmers. Dependent types are more powerful, but they aren't free from complications. For instance, unifying the type and value languages willy-nilly can cause trouble if you want your value language to be Turing-complete, because now type-level computation can diverge too! In a language based on System F-omega, type-level computation is guaranteed not to diverge, because its type level is the simply typed lambda calculus. Some use cases might warrant providing more powerful type-level computation facilities (e.g. calculating the shapes of multidimensional matrices), but it isn't clear to me that the full power of a Martin-Loef-style dependent type theory is needed.