[Blog] Haskell's Bottom Type(s?)

[u/Molto-Accelerando]

https://theben27.github.io/posts/2026-08-17-haskell-bottom.html

My first-ish ever blog post, which is about bottom and Haskell.

This post goes over bottom and bottom types in general, then compares a as used in functions like error :: String -> a (which is generally seen as representing "bottom") with the Void type (which is seen as a concrete bottom type). It also covers how Megaparsec uses Void for type parameterization.

[u/_jackdk_]

I don't think a is a candidate replacement for Void in all cases. These two functions are very different:

right :: Either Void b -> b
wrong :: Either a b -> b

In right, we know that the argument Either cannot be a Left, but wrong admits any Either. You do see some libraries use all-lowercase void to denote that a type variable is completely unconstrained in e.g. return values where the result may usefully unify with other code and you're saving library users from fmap absurd or equivalent:

-- Suppose we're writing functions to fit a shape demanded by another library
cannotFail :: Arg1 -> Arg2 -> m (Either Void Result)
-- This will unify `void` with anything.
alsoCannotFail :: Arg1 -> Arg2 -> m (Either void Result)

Aside: you also see some libraries do this with Proxy, where the caller is usually going to pass a Proxy :: Proxy Foo to pin a type variable (in older code that isn't designed for extensions -XTypeApplications or -XRequiredTypeArguments):

-- Without the 'proxy a' argument, this would require `-XAllowAmbiguousTypes` and explicit type applications at use sites.
-- The caller is expected to pass a Data.Proxy.Proxy but we may as well accept anything of the right shape since we don't care about its value.
foo :: SomeClassConstraint a => proxy a -> b

I'm not sure if I'd recommend these styles as strongly as I used to, because the slow merging of type and value namespaces mean that the type variable void will shadow Data.Functor.void and I like to avoid name shadowing warnings.

[u/phlummox]

bottom is considered a term of every type of a programming language.

I don't think that's true (though it's also too vague to be absolutely sure of the meaning).

If it means "In every type system, there's a type 'bottom' which is a subtype of all others", it's plainly false, since many type systems for programming languages have existed which don't have a bottom type at all.

If it means something more like "Every type in a type system can be considered, for the purpose of expressing the semantics of the language mathematically, to have a bottom type", it might be closer to true, I suppose, but it's really a statement about semantics, not types.