[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?