5 ms·

This would not have happened in a language with a proper type system as the type checker would have rejected the program at compile time.

saagarjha 7y ago
Type confusion and memory corruption is still possible in statically-typed languages, generally due to bugs in the runtime.
_ZeD_ 7y ago
literally 3 seconds with google:"ghc segfault" https://github.com/lehins/ghc-segfault https://github.com/lehins/ghc-segfault
shakna 7y ago
> This would not have happened in a language with a proper type system as the type checker would have rejected the program at compile time. How about in Rust, then? [0] Bugs happen in every language. When memory corruption occurs, you can segfault. [0] https://users.rust-lang.org/t/rust-guarantees-no-segfaults-with-only-safe-code-but-it-segfaults-stack-overflow/4305 https://users.rust-lang.org/t/rust-guarantees-no-segfaults-w...
- dependenttypes 7y ago
  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.

saagarjha 7y ago

Type confusion and memory corruption is still possible in statically-typed languages, generally due to bugs in the runtime.

_ZeD_ 7y ago

literally 3 seconds with google:"ghc segfault" https://github.com/lehins/ghc-segfault https://github.com/lehins/ghc-segfault

shakna 7y ago

> This would not have happened in a language with a proper type system as the type checker would have rejected the program at compile time. How about in Rust, then? [0] Bugs happen in every language. When memory corruption occurs, you can segfault. [0] https://users.rust-lang.org/t/rust-guarantees-no-segfaults-with-only-safe-code-but-it-segfaults-stack-overflow/4305 https://users.rust-lang.org/t/rust-guarantees-no-segfaults-w...

dependenttypes 7y ago
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.