3 ms·

I like that GADTs are a good example of "lightweight dependent types". You don't need to use full-blown dependent types to achieve the following: - type-safe A

I like that GADTs are a good example of "lightweight dependent types". You don't need to use full-blown dependent types to achieve the following: - type-safe AST representations of a language - type-safe encoding of lambda calculus and an eval function that will only accept _closed terms_ (i.e. no free variables!) In Coq, everything is defined in the GADT style and with dependent types you have an explosion of possibilities: - length-indexed vectors - dependently-typed red-black trees - inductive proofs! just to name a few.

AnthonBerg 5y ago
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!
fho 5y ago
I am full pro-Haskell, have used GADTs to define ASTs before and just love length-indexed everything (i.e. nd-matrices) ... but reading your comment I guess somebody who never came in contact with "modern languages" has no idea what you are talking about :-)

AnthonBerg 5y ago

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!

fho 5y ago

I am full pro-Haskell, have used GADTs to define ASTs before and just love length-indexed everything (i.e. nd-matrices) ... but reading your comment I guess somebody who never came in contact with "modern languages" has no idea what you are talking about :-)