What is GHC.Stack.Types.HasCallStack

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

2 Likes

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.

3 Likes

Yeah, I like the idea of the Partial constraint.

2 Likes

HasCallstack was introduced as a mechanism to allow authors to precisely control the generation of callstacks when an exception happens.

As you can see, it’s a bit finicky and not everyone is happy with the current design. But at least we get callstacks now!

2 Likes

That would seem to be a reasonable summary of this issue:

It’s also appeared here:

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.

In all cases, no, I doubt it. It is implemented as an implicit parameter, that is, it really is an argument to each function that it annotates.

Yeah, look at the docs: GHC.Stack

More specifically:

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.

Thankfully we are getting out of this with this recently accepted GHC Proposal: https://github.com/bgamari/ghc-proposals/blob/stacktraces/proposals/0000-exception-backtraces.rst

6 Likes

Why is head not defined as a safe function instead?

This may help to explain that:

(Note: it’s a long read…)

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.

1 Like

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

3 Likes

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?

3 Likes

A “noise word” ?

https://web.archive.org/web/20221205155031/https://mail.mozilla.org/pipermail/rust-dev/2013-April/003926.html

But this is getting somewhat off-topic (perhaps for a new thread in the New Year…) - the question:

has been answered here:

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.

From looking at the PureScript documentation, it appears unsafePartial works by throwing an exception. For Haskell, that suggests:

partialToException :: (Partial => a) -> b
partialToException x = throw (PartiallyDefined (fromPartial x))

with a suitable invocation of catch in IO to deal with the exception accordingly. Now compare that to the current definition of Prelude.error :

error ::  ...  HasCallStack => [Char] -> a
error s = raise# (errorCallWithCallStackException s ?callStack)

…let’s just rename HasCallStack to Partial - problem solved!

1 Like

RE: partialToException

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)

2 Likes

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

3 Likes