5 ms·

> The idea that compile-time checks is much better than runtime checks is also not obvious (Java's and other commercial languages nonsense about type safety asi

> The idea that compile-time checks is much better than runtime checks is also not obvious (Java's and other commercial languages nonsense about type safety aside - Java is no more safe than CL). Runtime checks will only trip up if you happen to hit a code path the introduces an incorrect type. This may only occur in some extremely rare scenario that you never pick up in testing. Compile time type checking allows you to prove that your program is definitely type safe, with 100% certainty.

dschiptsov 12y ago
I am not sure that this assertion is true for user-defined ADTs, which is the essence of programming.
- zak_mc_kracken 12y ago
  It's absolutely true for any code that's referentially transparent, regardless of whether it uses user-defined ADTs or any other construct.
- wyager 12y ago
  >I am not sure that this assertion is true for user-defined ADTs Depends what you mean. It's safe in the sense that you will never get a type error. In Haskell terms, it's possible to write a function that's not total (e.g. not implemented for all possible data constructors of a type), which can then crash or fail to terminate. For example, "head" will crash on an empty list (duh). However, this is easy to avoid, and type safety in Haskell always holds true, as do all the other guarantees the compiler makes (like referential transparency).
  - dschiptsov 12y ago
    Yes, the head of [] is the best example. That is what I mean. Thanks for a clarification. Absence of type errors is not safety, it is absence of type errors.)
    - wyager 12y ago
      OK, cool. Of course, almost no languages check for totality. Agda is one of the few that does it by default. I think Rust makes you complete all pattern matches too. However, if you do get a pattern match failure, one of two things is true: 1. You can easily fix it by accounting for all patterns (or adding a default match) 2. Your program model is conceptually broken and you should probably find a new model that accounts for all possible patterns. Much easier to deal with than a type error :)
      - scriptdevil 12y ago
        GHC Haskell has -fwarn-incomplete-patterns . Are you talking about something else?
      - vertex-four 12y ago
        > I think Rust makes you complete all pattern matches too. It does, although for Option and Result, there's .unwrap() which simply exits the program (through fail!()) on None/error. The fact that you can do this is practical, although could potentially train bad habits.
      - dllthomas 12y ago
        Strictly speaking, "totality" is asking for more than just exhaustiveness in pattern matching (all manner of languages let you check exhaustiveness). For totality, you also have to prove termination for all inputs, which means your language (or sub-language) is not Turing complete. Though these days I've been saying "Turing complete" is a bug, not a feature, provided you can accomplish your aims without it.
    - creichert 12y ago
      ghc has an RTS option to locate errors of that nature: -xc (Only available when the program is compiled for profiling.) When an exception is raised in the program, this option causes a stack trace to be dumped to stderr. This can be particularly useful for debugging: if your program is complaining about a head [] error and you haven't got a clue which bit of code is causing it, compiling with -prof -fprof-auto and running with +RTS -xc -RTS will tell you exactly the call stack at the point the error was raised. http://www.haskell.org/ghc/docs/7.8.3/html/users_guide/runtime-control.html http://www.haskell.org/ghc/docs/7.8.3/html/users_guide/runti...

dschiptsov 12y ago

I am not sure that this assertion is true for user-defined ADTs, which is the essence of programming.

zak_mc_kracken 12y ago
It's absolutely true for any code that's referentially transparent, regardless of whether it uses user-defined ADTs or any other construct.
wyager 12y ago
>I am not sure that this assertion is true for user-defined ADTs Depends what you mean. It's safe in the sense that you will never get a type error. In Haskell terms, it's possible to write a function that's not total (e.g. not implemented for all possible data constructors of a type), which can then crash or fail to terminate. For example, "head" will crash on an empty list (duh). However, this is easy to avoid, and type safety in Haskell always holds true, as do all the other guarantees the compiler makes (like referential transparency).
- dschiptsov 12y ago
  Yes, the head of [] is the best example. That is what I mean. Thanks for a clarification. Absence of type errors is not safety, it is absence of type errors.)
  - wyager 12y ago
    OK, cool. Of course, almost no languages check for totality. Agda is one of the few that does it by default. I think Rust makes you complete all pattern matches too. However, if you do get a pattern match failure, one of two things is true: 1. You can easily fix it by accounting for all patterns (or adding a default match) 2. Your program model is conceptually broken and you should probably find a new model that accounts for all possible patterns. Much easier to deal with than a type error :)
    - scriptdevil 12y ago
      GHC Haskell has -fwarn-incomplete-patterns . Are you talking about something else?
    - vertex-four 12y ago
      > I think Rust makes you complete all pattern matches too. It does, although for Option and Result, there's .unwrap() which simply exits the program (through fail!()) on None/error. The fact that you can do this is practical, although could potentially train bad habits.
    - dllthomas 12y ago
      Strictly speaking, "totality" is asking for more than just exhaustiveness in pattern matching (all manner of languages let you check exhaustiveness). For totality, you also have to prove termination for all inputs, which means your language (or sub-language) is not Turing complete. Though these days I've been saying "Turing complete" is a bug, not a feature, provided you can accomplish your aims without it.
  - creichert 12y ago
    ghc has an RTS option to locate errors of that nature: -xc (Only available when the program is compiled for profiling.) When an exception is raised in the program, this option causes a stack trace to be dumped to stderr. This can be particularly useful for debugging: if your program is complaining about a head [] error and you haven't got a clue which bit of code is causing it, compiling with -prof -fprof-auto and running with +RTS -xc -RTS will tell you exactly the call stack at the point the error was raised. http://www.haskell.org/ghc/docs/7.8.3/html/users_guide/runtime-control.html http://www.haskell.org/ghc/docs/7.8.3/html/users_guide/runti...