4 ms·

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.)
  - 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...
  - 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.
  - zoomerang 12y ago
    Well yes and no. GHC does a pretty good job of warning you when you're missing a potential option in a pattern match, and it's generally pretty easy to write code that avoids partial functions as a result. But still, you're right - it's not 100% safety, and will only give you a warning. There's no reason to throw the baby out with the bathwater though, since 90% safety is a hell of a lot better than 0% safety. Personally I'm keen to see mainstream languages adopt better totality checking for that exact reason - my fantasy language would enforce that `main` is always a total function* *(For this fantasy language, I'd probably allow infinite recursion to still exist, since the halting problem is theoretically impossible to solve without introducing a lot of pain to prove that your code will actually terminate, and that level of totality checking is often counter-productive for general-purpose code)

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.)
- 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...
- 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.
- zoomerang 12y ago
  Well yes and no. GHC does a pretty good job of warning you when you're missing a potential option in a pattern match, and it's generally pretty easy to write code that avoids partial functions as a result. But still, you're right - it's not 100% safety, and will only give you a warning. There's no reason to throw the baby out with the bathwater though, since 90% safety is a hell of a lot better than 0% safety. Personally I'm keen to see mainstream languages adopt better totality checking for that exact reason - my fantasy language would enforce that `main` is always a total function* *(For this fantasy language, I'd probably allow infinite recursion to still exist, since the halting problem is theoretically impossible to solve without introducing a lot of pain to prove that your code will actually terminate, and that level of totality checking is often counter-productive for general-purpose code)