[zoomerang]

> 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]

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

[wyager]

>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]

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.)

[zoomerang]

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)

[wyager]

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 :)

[dllthomas]

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.

[vertex-four]

> 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.

[scriptdevil]

GHC Haskell has -fwarn-incomplete-patterns . Are you talking about something else?

[creichert]

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/runti...

[zak_mc_kracken]

It's absolutely true for any code that's referentially transparent, regardless of whether it uses user-defined ADTs or any other construct.