4 ms·

Useful take, thanks! I assume it varies, but I find Idris' dependent type system to be easier to reason about and understand than non-dependent ones I've worke

Useful take, thanks! I assume it varies, but I find Idris' dependent type system to be easier to reason about and understand than non-dependent ones I've worked with (say, OCaml and Haskell). Even if Idris can be judged as strictly more powerful in that regard. There's a sense of a closed loop of consistency and a smaller, tighter set of thought patterns that apply both on this side and the other side – whatever those sides may be, say, values vs. types, compilation vs. runtime, AST vs. raw syntax, parsing vs. printing… It's an explosion of possibilities!, but as it's a shaped charge of constructive and intuitionistic principles it mostly just blows up shackles and clears the air :)

siraben 5y ago
Yes! I love the consistency of dependent types. You don't need separate declarations for type aliases or a dozen language extensions to do some type-level evaluation, it's quite uniform. > It's an explosion of possibilities!, but as it's a shaped charge of constructive and intuitionistic principles it mostly just blows up shackles and clears the air :) Indeed, I feel like we are just getting started finding the right "design patterns" for working with dependently typed programs. It's sort of a Wild West of styles in the Coq world currently, IMO, which is great when something is well designed but terrible when using a theorem demands you prove some clearly obvious precondition (e.g. Riemann integration in the stdlib is a pain to work with).
- AnthonBerg 5y ago
  𝖙𝖍𝖊 𝖔𝖙𝖍𝖊𝖗 𝖘𝖎𝖉𝖊: Having expressibility of Riemann integration near a stdlib at all is marvelous!