4 ms·

I said "a language with a proper type system". Rust is not one such language.

by dependenttypes 7y ago

Znafon 7y ago
Can you give an example of such language so we don't have to guess? Apparently neither Rust, Haskell nor Go fit.
- dependenttypes 7y ago
  check my username
shakna 7y ago
You'll need to define "proper type system" then. At a guess, you want something with dependent types? Like Idris, or Haskell. You already have a Haskell example. This [0] release of Idris fixed a segfault when concatenating strings. Maybe you meant a language that is proven from the ground up. Like CakeML. You can find a segfault example here [1]. Maybe you meant a language with an algebraic type system like Ada. You can find a segfault example here [2]. Maybe you meant something like Dotty (Research for the next version of Scala). You can find a segfault example here [3]. In short: You'll need to describe what you believe to be a "proper" type system, and name the languages you think fit that description, or no one can have a conversation with you. [0] https://www.idris-lang.org/idris-1-1-1-released/ https://www.idris-lang.org/idris-1-1-1-released/ [1] https://github.com/CakeML/cakeml/issues/438 https://github.com/CakeML/cakeml/issues/438 [2] https://stackoverflow.com/questions/56227629/segmentation-fault-during-runtime-elaboration-ada https://stackoverflow.com/questions/56227629/segmentation-fa... [3] https://github.com/lampepfl/dotty/pull/7466/ https://github.com/lampepfl/dotty/pull/7466/
- 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.

I said "a language with a proper type system". Rust is not one such language.

Znafon 7y ago

Can you give an example of such language so we don't have to guess? Apparently neither Rust, Haskell nor Go fit.

dependenttypes 7y ago
check my username

shakna 7y ago

You'll need to define "proper type system" then. At a guess, you want something with dependent types? Like Idris, or Haskell. You already have a Haskell example. This [0] release of Idris fixed a segfault when concatenating strings. Maybe you meant a language that is proven from the ground up. Like CakeML. You can find a segfault example here [1]. Maybe you meant a language with an algebraic type system like Ada. You can find a segfault example here [2]. Maybe you meant something like Dotty (Research for the next version of Scala). You can find a segfault example here [3]. In short: You'll need to describe what you believe to be a "proper" type system, and name the languages you think fit that description, or no one can have a conversation with you. [0] https://www.idris-lang.org/idris-1-1-1-released/ https://www.idris-lang.org/idris-1-1-1-released/ [1] https://github.com/CakeML/cakeml/issues/438 https://github.com/CakeML/cakeml/issues/438 [2] https://stackoverflow.com/questions/56227629/segmentation-fault-during-runtime-elaboration-ada https://stackoverflow.com/questions/56227629/segmentation-fa... [3] https://github.com/lampepfl/dotty/pull/7466/ https://github.com/lampepfl/dotty/pull/7466/

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.