Why discarded values are () instead of ⊥ in Haskell?

Question

Howcome in Haskell, when there is a value that would be discarded, () is used instead of ⊥?

Examples (can't really think of anything other than IO actions at the moment):

mapM_ :: (Monad m) => (a -> m b) -> [a] -> m ()
foldM_ :: (Monad m) => (a -> b -> m a) -> a -> [b] -> m ()
writeFile :: FilePath -> String -> IO ()

Under strict evaluation, this makes perfect sense, but in Haskell, it only makes the domain bigger.

Perhaps there are "unused parameter" functions d -> a which are strict on d (where d is an unconstrained type parameter and does not appear free in a)? Ex: seq, const' x y = yseqx.

Answer 1

You're getting confused between types and values.

In writeFile :: FilePath -> String -> IO (), the () is the unit type. The value you get for x by doing x <- writeFile foo bar in a do block is (normally) the value (), which is the sole non-bottom inhabitant of the type ().

⊥ OTOH is a value. Since ⊥ is a member of every type, it's also usable as a value for the type (). If you're discarding that x above without using it (we normally don't even extract it into a variable), it may very well be ⊥ and you'd never know. In that sense you already have what you want; if you're ever writing a function whose result you expect to be always ignored, you could use ⊥. But since ⊥ is a value of every type, there is no type ⊥, and so there is no type IO ⊥.

But really, they represent different conceptual things. The type () is the type of values that contain zero information (which is why there is only one value; if there were two or more values then () values would contain at least as much information as values of Bool). IO () is the type of IO actions that generate a value with no information, but may effects that will happen as a result of generating that non-informative value.

⊥ is in some sense a non-value. 1 `div` 0 gives ⊥ because there is no value that could be used as the result of that expression which satisfies the laws of integer division. Throwing an exception gives ⊥ because functions that contain exception throws do not give you a value of their type. Non-termination gives ⊥ because the expression never terminates with a value. ⊥ is a way of treating all of these non-values as if they were a value for some purposes. As far as I can tell it's mainly useful because Haskell's laziness means that ⊥ and a data structure containing ⊥ (i.e. [⊥]) are distinguishable.

The value () is not like the cases where we use ⊥. writeFile foo bar doesn't have an "impossible value" like return $ 1 `div` 0, it just has no information in its value (other than that contained in the monadic structure). There are perfectly sensible things I could do with the () I get from doing x <- writeFile foo bar; they're just not very interesting and so nobody ever does them. This is distinctly different from x <- return $ 1 `div` 0, where doing anything with that value has to give me another ill-defined value.

Answer 2

() is ⊤, i.e. the unit type, not the ⊥ (the bottom type). The big difference is that the unit type is inhabited, so that it has a value (() in Haskell), on the other hand, the bottom type is uninhabited, so that you can't write functions like that:

absurd : ⊥
absurd = -- no way

Of course you can do this in Haskell since the "bottom type" (there is no such thing, of course) is inhabited here with undefined. This makes Haskell inconsistent.

Functions like this:

disprove : a → ⊥
disprove x = -- ...

can be written, it is the same as

disprove : ¬ a
disprove x = -- ...

i.e. it disproving the type a, so that a is an absurd.

In any case, you can see how the unit type is used in different languages, as () :: () in Haskell, () : unit in ML, () : Unit in Scala and tt : ⊤ in Agda. In languages like Haskell and Agda (with the IO monad) functions like putStrLn should have a type String → IO ⊤, not the String → IO ⊥ since this is an absurd (logically it states that there is no strings that can be printed, this is just not right).

---

DISCLAIMER: previous text use Agda notation and it is more about Agda than Haskell.

In Haskell if we have

data Void

It doesn't mean that Void is uninhabited. It is inhabited with undefined, non-terminating programs, errors and exceptions. For example:

data Void

instance Show Void where
  show _ = "Void"

data Identity a = Identity { runIdentity :: a }

mapM__ :: (a -> Identity b) -> [a] -> Identity Void
mapM__ _ _ = Identity undefined

then

print $ runIdentity $ mapM__ (const $ Identity 0) [1, 2, 3]
-- ^ will print "Void".
case runIdentity $ mapM__ (const $ Identity 0) [1, 2, 3] of _ -> print "1"
-- ^ will print "1".
let x = runIdentity $ mapM__ (const $ Identity 0) [1, 2, 3]
x `seq` print x
-- ^ will thrown an exception.

But it also doesn't mean that Void is ⊥. So

mapM_ :: Monad m => (a -> m b) -> [a] -> m Void

where Void is decalred as empty data type, is ok. But

mapM_ :: Monad m => (a -> m b) -> [a] -> m ⊥

is nonsence, but there is no such type as ⊥ in Haskell.

Answer 3

I would like to point out one severe downside to writing one particular form of returning ⊥: if you write types like this, you get bad programs:

mapM_ :: (Monad m) => (a -> m b) -> [a] -> m z

This is way too polymorphic. As an example, consider forever :: Monad m => m a -> m b. I encountered this gotcha a long time ago and I'm still bitter:

main :: IO ()
main = forever putStrLn "This is going to get printed a lot!"

The error is obvious and simple: missing parentheses.

• It typechecks. This is exactly the sort of error that the type system is supposed to catch easily.
• It silently infinite loops at runtime (without printing anything). It is a pain to debug.

Why? Well, because r -> is a monad. So m b matches virtually anything. For example:

forever :: m a -> m b
forever putStrLn :: String -> b
forever putStrLn "hello!" :: b -- eep!
forever putStrLn "hello" readFile id flip (Nothing,[17,0]) :: t -- no type error.

This sort of thing inclines me to the view that forever should be typed m a -> m Void.

Answer 4

I think this is because you need to specify the type of the value to be discarded. In Haskell-98, () is the obvious choice. And as long as you know the type is (), you may as well make the value () as well (presuming evaluation proceeds that far), just in case somebody tries to pattern-match on it or something. I think most programmers don't like introducing extra ⊥'s into code because it's just an extra trap to fall into. I certainly avoid it.

Instead of (), it is possible to create an uninhabited type (except by ⊥ of course).

{-# LANGUAGE EmptyDataDecls #-}

data Void

mapM_ :: (Monad m) => (a -> m b) -> [a] -> m Void

Now it's not even possible to pattern-match, because there's no Void constructor. I suspect the reason this isn't done more often is because it's not Haskell-98 compatible, as it requires the EmptyDataDecls extension.

Edit: you can't pattern-match on Void, but seq will ruin your day. Thanks to @sacundim for pointing this out.

Answer 5

So, maybe we could have the following signatures:

mapM_     :: (Monad m) => (a -> m b) -> [a] -> m z
foldM_    :: (Monad m) => (a -> b -> m a) -> a -> [b] -> m z
writeFile :: FilePath -> String -> IO z

We'd reimplement the functions in question so that any attempt to bind the z in m z or IO z would bind the variable to undefined or any other bottom.

What do we gain? Now people can write programs that force the undefined result of these computations. How is that a good thing? All it means is that people can now write programs that fail to terminate for no good reason, that were impossible to write before.

Answer 6

Well, bottom type literally means an unterminating computation, and unit type is just what it is - a type inhabited with single value. Clearly, monadic computations usually meant to be finished, so it simply doesn't make sense to make them return undefined. And, of course, it is simply a safety measure - just like John L said, what if someone pattern matches on monadic result? So monadic computations return the 'lowest' possible (in Haskell 98) type - unit.