3 ms·
I meant dependent types a la Agda, Coq etc that you can use for proving essentially arbitrary properties. Scala and Haskell do not have this.
by mafribe 11y ago
I meant dependent types a la Agda, Coq etc that you can use for proving essentially arbitrary properties. Scala and Haskell do not have this.
- lmm 11y agoI don't understand the distinction you're drawing. Idris' type level functions are easier to write than Scala's but they don't seem to be able to do anything that Scala ones can't.