`head` absolutely doesn't know something the compiler doesn't, because there is no guarantee the user is using it correctly!
The fact that https://doc.rust-lang.org/std/vec/struct.Vec.html#method.pop returns Option<T> really says it all. We're not trying to be perfect, we're just trying to be no worse than Rust, which shouldn't be a high bar at all.
I wrote https://github.com/ghc-proposals/ghc-proposals/pull/351 to address just these sorts of issues, and not the harder ones people confuse them with.
I don't understand what you mean by this.
>`head` absolutely doesn't know something the compiler doesn't, because there is no guarantee the user is using it correctly!
But the user can use `head` when they know that the list they are handling is non-empty (but then they can also opt for `Data.List.NonEmpty`). I never said the partial function itself carried any knowledge - only that it was a necessary escape hatch for cases where the programmer has the knowledge to use it correctly.
>We're not trying to be perfect, we're just trying to be no worse than Rust, which shouldn't be a high bar at all.
I'm not opposed to that - and I don't see why you would think that I am. I'm just arguing that, in response to the question made by the other commenter, we can't "do without" partial functions entirely. That doesn't mean I believe they belong everywhere, and certainly not in most APIs.
I think that GP tries to say the escape hatches are not the problem. "error" and "undefined" are fine (we can check for undefined not being in production code, and errors, well, could be implemented as a "die" or "halt").
But head though... It should return a Maybe wrapped value! And as you say the other option is nonempty lists a.k.a. "(a, [a])".
> only that it was a necessary escape hatch for cases where the programmer has the knowledge to use it correctly.
Well the docs do not present head as an escape hatch out of Haskell iron type system! It's documented rather innocently [1] (search for head). Unlike unsafePerformIO[2] and the likes, which have whole epistols detailing their danger.
> I'm just arguing that, in response to the question made by the other commenter, we can't "do without" partial functions entirely.
Please consider escape hatches differently from basic stuff like head and you see we argue for the same end result. Head is plain bad, should be removed or annotated as the smelly thing it is. maybeHead and non-empty-collections are the way fwd there, would you agree?
1: http://hackage.haskell.org/package/base-4.3.1.0/docs/Prelude...
2: https://hackage.haskell.org/package/base-4.14.0.0/docs/Syste...
I don't get what you're trying to say. I never said that head was good. The discussion about head is a sidetrack to the original question, which is "To what extend can we do without [partial functions]?", and to which my answer is "we can't do without". head is not a good example of a partial function, and its existence doesn't conflict with the idea that good partial functions are a necessary part of the language.
You don't need an advanced checker for partial functions - the link you use is discussing proving termination, but total vs partial functions just requires checking whether the function is defined for all arguments, which is easy and something that GHC can already do.
And to be honest, I'm not sure we can do without. Partial functions and `error` (or `undefined`) are necessary escape hatches for the programmer who knows something the compiler doesn't. Partial functions should probably not end up in any APIs (and definitely not in the Prelude), but they are still an important part of the language.
Only the introduction of dependent typing has the possibility of really eliminating partial functions for good.