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.)
headIO :: [a] -> IO a
headIO (x:_) = return x
headIO [] = throwIO (errorCallWithoutCallStackException "empty list!" )
import Control.Exception(evaluate) -- :: a -> IO a
head :: [a] -> a
head (x:_) = x
head [] = throw (errorCallWithoutCallStackException "empty list!")
headIO :: [a] -> IO a
headIO = evaluate . head
Is there one? I don’t feel fully confident in the distinction between precise and imprecise exceptions, but my understanding of evaluate is that it’ll turn an error in the reduction of its argument into an exception in IO, and throwIO simply starts with an exception in IO, so my guess is that they would do the same thing.
Well, this is very close to what a Kleisli arrow in MonadError monad already does. The only thing it cannot model is totality-polymorphic composition, which is a very challenging notion (at least for linear types).
Oh, absolutely! The only difference between using Kleisli arrows or function arrows to model this is ergonomic. Ergonomics is what drove the decision to make the Partial class, though, so if we’re solving the ergonomic problem with Kleisli composition by adding something for the particular case of Kleisli arrows in the partiality monad, the above proposal is what I’d recommend over a Partial class.
Explanation for those unfamiliar with PureScript: the language’s integration with Partial is such that an incomplete case expression requires a Partial ‘instance’ in scope (there are no such instances in fact, but having the constraint in an outer scope discharges the requirement, and unsafePartial ultimately tells the lie that there is one). So instead of
foo :: MonadError e m => [a] -> m a
foo xs = case xs of
h:_ -> pure h
_ -> throwError ...
one writes
foo :: Partial => [a] -> a
foo xs = case xs of
h:_ -> h
For larger functions, this is a big deal; the Partial constraint can be requested once and then regular function composition suffices for everything inside.
It’s a neat thought, but again, the difficulty is that the Partial constraint isn’t specific enough about which function arrows have the partiality attached to them, and that ultimately leads to the problem I was highlighting. The challenge is to solve the problem with a similar lack of intrusiveness (which is the problem with Kleisli-ing everything). Modified arrows are the only idea I have that seems like it could do that.
My initial though was instead of a constraint have an implicit parameter like ?unPartial :: Maybe a -> a (which can call error if needs to be, that is the caller decision) but it probably doesn’t work either.
