It’s a wart. You shouldn’t have to change the type signature to get a proper error message.
It’s also not really an exhaustive mechanism to mark partial functions. A partial function may or may not have it. You can assign it to a total function too.
What’s the alternative? Implicitly add a HasCallStack to every definition?
It’s also not really an exhaustive mechanism to mark partial functions. A partial function may or may not have it. You can assign it to a total function too.
That’s the same with pretty much every Haskell construct isn’t it? A function with a HasCallStack constraint may or may not use it (by throwing an exception). A function may or may not use its argument. A value of type IO a may or may not do IO.
I don’t know. But it seems to me like implementation details leaking. As an end user I don’t really care what magic the compiler conjures to present me with reasonable call stack in the error message.
Why is this offloaded to core libraries?
Yeah, although “maybe partial or not” is really not useful to end users or is it? “This function has access to IO, but may not actually do IO” isn’t that confusing to me.
There was a discussion once to add a Partial constraint to base, following a HasCallStack discussion. So yeah.
The documentation says it is a lightweight method of obtaining a partial call-stack which probably means that it is not zero cost. Can GHC optimize the book-keeping away for functions that do not explicitly use this constraint? If not, I agree with @hasufell that it is pointless to make it explicit in the type signature.
NOTE: The implicit parameter ?callStack :: CallStack is an implementation detail and should not be considered part of the CallStack API, we may decide to change the implementation in the future.
Not sure how much Iike that wording, given how prominently HasCallStack is exposed.
It was specified 35 years ago, drawing on decades of precedent, probably going back all the way to Lisp, when programmers and language designers had bigger things to worry about. It’s debatable whether it would be designed this way if Haskell were started today. For example, Purescript’s version of head has a Partial constraint that can only be dispatched with a use of unsafePartial.
As Tom says, that decision is out of our hands, so we have to make do with the tools we have now: using uncons if List must be the interface type, or using NonEmpty in order to enforce the invariants earlier in the program.
PureScript has this, and we’re probably stuck with it at this point, but I think it was a bad decision.
The problem with encoding partiality as a constraint is that unsafePartial head (where unsafePartial :: (Partial => a) -> a) resolves the constraint to the compiler’s satisfaction without actually reducing the thing that is partial (the intent is that you’d always call unsafePartial (head foo) instead, but mistakes happen and type checkers are for catching them). You’re left with something having the type of a pure function, and you can pass that pure function anywhere else and it may blow up on you there.
And you can say, well, you used something called unsafe somewhere in your code; any subsequent blow-ups are on you. But there’s no way to use Partial-constrained types without using unsafePartial somewhere in your code, so this amounts to always knowing which functions are partial and manually keeping track of when they’re fully reduced—which is exactly what we’d have to do if partiality wasn’t encoded in the type system at all, so what have we gained?
Perhaps it would be illustrative to examine the difference between unsafePartial and unsafePerformIO.
If we want to use IO in Haskell we have a “proper” way of doing so, which is just to plumb it all the way to main :: IO (). There is such corresponding way of using Partial, because the type of main is not Partial => Effect Unit. That means users using Partial are forced to use unsafePartial at some point in their program. If Haskell forced users to use unsafePerformIO in order to do IO that would also be very bad (actually, worse).
Would the situation be better if instead of unsafePartial the way of interpreting Partial => was partialToException :: (Partial => a) -> Effect a? The equivalent in Haskell would be partialToException :: (Partial => a) -> IO a. We still wouldn’t have the property that evaluate <=< partialToException removes the partiality, but at least the partiality is stuck in IO. On the other hand, this wouldn’t allow us to “mark” safe usages of, e.g., head and return to the pure world.
I don’t see the purpose of this. If the only way to invoke a partial function is via IO, why not just force partial functions to be IO and use throwIO?
The whole point of partial functions is the developer knowing that a certain branch is unreachable, but can’t prove it via the type system. So me writing
newtype NonEmptySet a = NonEmptySet (Set a)
toList :: NonEmptySet a -> NonEmpty a
toList (NonEmptySet s) =
case nonEmpty (Set.toList s) of
Nothing -> error "unreachable"
Just l -> l
is morally correct, provided I don’t export the constructor for NonEmptySet. It would be quite sad if the only way to call toList is via IO, because it would leak the implementation (that I’m reusing Set instead of creating a NonEmpty version of the Set ADT that makes illegal states unrepresentable)
I don’t think that’s the correct model. Partiality isn’t a property of a term; it’s a property of a function. A term either reduces to bottom or does not. A function may return a bottom on some inputs and be defined on others.
If I have a term that produces IO ([a] -> a), I understand that type as telling me that in order to get to the function within, I must suffer any sort of side effect. But from inside the lambda to which that term is >>='d, the term of type [a] -> a is pure—regardless of how many times I call it, or on which inputs I call it, it will not create any more side effects. If I want to express that the inner function might cause more side effects, I need to Kleisli it: IO ([a] -> IO a).
With head :: Partial => [a] -> a and your proposed partialToException, I’d have partialToException head :: IO ([a] -> a). But the term head isn’t the thing that can cause problems; it’s the application of head to an empty list. So for the reasons I stated above, this doesn’t capture the correct property, that the term of type [a] -> a that gets bound in a lambda is still partial and needs to be handled with care.
The correct thing, using existing tools, is a Kleisli: headIO :: [a] -> IO a, or much more conventionally, headMay :: [a] -> Maybe a. But for someone who is willing to invest language complexity to get better ergonomics than that, I would want partiality to be expressed similarly to how Linear Haskell expresses linearity, as a modifier on the function type itself. With a few new language rules such as ‘the inferred type of a lambda that directly encloses an application of a partial function is partial’, totality-polymorphic function composition, and both a Kleisli-producing applyOrThrowIO :: Exception e => e -> (a %Partial -> b) -> a -> IO band an unsafeTotal :: (a %Partial -> b) -> a -> b for when you can’t prove totality to the type checker but you know you have it, this would have… well, exactly as many problems as Linear Haskell currently has. But presumably those are being worked on.
(The Linear Haskell connection is supported in my mind by the idea that the affine/linear distinction is ‘dual’—and I use the scare quotes only because I’m not enough of an expert to assert this confidently—to the partial/total distinction. A linear function must use its argument once, while an affine function might not use it at all. Dually, a total function must use its continuation once, while a partial function might not use it at all, considering throwing an error as escaping to some other continuation.)