2 ms·
You can trivially prove bottom in Haskell. Something like Agda or Idris would indeed fit the bill better. Anyway, I said that this specific issue would not occ
by dependenttypes 7y ago
You can trivially prove bottom in Haskell. Something like Agda or Idris would indeed fit the bill better.
Anyway, I said that this specific issue would not occur in a language with dependent types -- where incorrect code would cause the implementation to crash. Not that it is impossible to have a buggy compiler that at certain cases produces segfaults.
- shakna 7y ago> Not that it is impossible to have a buggy compiler that at certain cases produces segfaults. That's exactly what happened here, however. The instance check was missing from the interpreter. Dependant types wouldn't have solved the underlying problem.