4 ms·

Type level arithmetic is sugar for clever GADTs, not full blown dependent types. Try to do things in Agda/Idris and come back to haskell, the expressiveness is

by Drup 11y ago

Type level arithmetic is sugar for clever GADTs, not full blown dependent types. Try to do things in Agda/Idris and come back to haskell, the expressiveness is not nearly comparable.

wyager 11y ago
Are Nats in agda and idris not also just GADT based peano numbers?
- Drup 11y ago
  The toyish version showed in tutorials, yes. The real stuff, no, it's just .. integers. And anyway, my point was that you can do much much more than type level arithmetic.