What's the absurd function in Data.Void useful for?

Question

The absurd function in Data.Void has the following signature, where Void is the logically uninhabited type exported by that package:

-- | Since 'Void' values logically don't exist, this witnesses the logical
-- reasoning tool of \"ex falso quodlibet\".
absurd :: Void -> a

I do know enough logic to get the documentation's remark that this corresponds, by the propositions-as-types correspondence, to the valid formula ⊥ → a.

What I'm puzzled and curious about is: in what sort of practical programming problems is this function useful? I'm thinking that perhaps it's useful in some cases as a type-safe way of exhaustively handling "can't happen" cases, but I don't know enough about practical uses of Curry-Howard to tell whether that idea is on the right track at all.

EDIT: Examples preferably in Haskell, but if anybody wants to use a dependently typed language I'm not going to complain...

Solution 1

Life is a little bit hard, since Haskell is non strict. The general use case is to handle impossible paths. For example

simple :: Either Void a -> a
simple (Left x) = absurd x
simple (Right y) = y

This turns out to be somewhat useful. Consider a simple type for Pipes

data Pipe a b r
  = Pure r
  | Await (a -> Pipe a b r)
  | Yield !b (Pipe a b r)

this is a strict-ified and simplified version of the standard pipes type from Gabriel Gonzales' Pipes library. Now, we can encode a pipe that never yields (ie, a consumer) as

type Consumer a r = Pipe a Void r

this really never yields. The implication of this is that the proper fold rule for a Consumer is

foldConsumer :: (r -> s) -> ((a -> s) -> s) -> Consumer a r -> s
foldConsumer onPure onAwait p 
 = case p of
     Pure x -> onPure x
     Await f -> onAwait $ \x -> foldConsumer onPure onAwait (f x)
     Yield x _ -> absurd x

or alternatively, that you can ignore the yield case when dealing with consumers. This is the general version of this design pattern: use polymorphic data types and Void to get rid of possibilities when you need to.

Probably the most classic use of Void is in CPS.

type Continuation a = a -> Void

that is, a Continuation is a function which never returns. Continuation is the type version of "not." From this we get a monad of CPS (corresponding to classical logic)

newtype CPS a = Continuation (Continuation a)

since Haskell is pure, we can't get anything out of this type.

Solution 2

Consider this representation for lambda terms parametrized by their free variables. (See papers by Bellegarde and Hook 1994, Bird and Paterson 1999, Altenkirch and Reus 1999.)

data Tm a  = Var a
           | Tm a :$ Tm a
           | Lam (Tm (Maybe a))

You can certainly make this a Functor, capturing the notion of renaming, and a Monad capturing the notion of substitution.

instance Functor Tm where
  fmap rho (Var a)   = Var (rho a)
  fmap rho (f :$ s)  = fmap rho f :$ fmap rho s
  fmap rho (Lam t)   = Lam (fmap (fmap rho) t)

instance Monad Tm where
  return = Var
  Var a     >>= sig  = sig a
  (f :$ s)  >>= sig  = (f >>= sig) :$ (s >>= sig)
  Lam t     >>= sig  = Lam (t >>= maybe (Var Nothing) (fmap Just . sig))

Now consider the closed terms: these are the inhabitants of Tm Void. You should be able to embed the closed terms into terms with arbitrary free variables. How?

fmap absurd :: Tm Void -> Tm a

The catch, of course, is that this function will traverse the term doing precisely nothing. But it's a touch more honest than unsafeCoerce. And that's why vacuous was added to Data.Void...

Or write an evaluator. Here are values with free variables in b.

data Val b
  =  b :$$ [Val b]                              -- a stuck application
  |  forall a. LV (a -> Val b) (Tm (Maybe a))   -- we have an incomplete environment

I've just represented lambdas as closures. The evaluator is parametrized by an environment mapping free variables in a to values over b.

eval :: (a -> Val b) -> Tm a -> Val b
eval g (Var a)   = g a
eval g (f :$ s)  = eval g f $$ eval g s where
  (b :$$ vs)  $$ v  = b :$$ (vs ++ [v])         -- stuck application gets longer
  LV g t      $$ v  = eval (maybe v g) t        -- an applied lambda gets unstuck
eval g (Lam t)   = LV g t

You guessed it. To evaluate a closed term at any target

eval absurd :: Tm Void -> Val b

More generally, Void is seldom used on its own, but is handy when you want to instantiate a type parameter in a way which indicates some sort of impossibility (e.g., here, using a free variable in a closed term). Often these parametrized types come with higher-order functions lifting operations on the parameters to operations on the whole type (e.g., here, fmap, >>=, eval). So you pass absurd as the general-purpose operation on Void.

For another example, imagine using Either e v to capture computations which hopefully give you a v but might raise an exception of type e. You might use this approach to document risk of bad behaviour uniformly. For perfectly well behaved computations in this setting, take e to be Void, then use

either absurd id :: Either Void v -> v

to run safely or

either absurd Right :: Either Void v -> Either e v

to embed safe components in an unsafe world.

Oh, and one last hurrah, handling a "can't happen". It shows up in the generic zipper construction, everywhere that the cursor can't be.

class Differentiable f where
  type D f :: * -> *              -- an f with a hole
  plug :: (D f x, x) -> f x       -- plugging a child in the hole

newtype K a     x  = K a          -- no children, just a label
newtype I       x  = I x          -- one child
data (f :+: g)  x  = L (f x)      -- choice
                   | R (g x)
data (f :*: g)  x  = f x :&: g x  -- pairing

instance Differentiable (K a) where
  type D (K a) = K Void           -- no children, so no way to make a hole
  plug (K v, x) = absurd v        -- can't reinvent the label, so deny the hole!

I decided not to delete the rest, even though it's not exactly relevant.

instance Differentiable I where
  type D I = K ()
  plug (K (), x) = I x

instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where
  type D (f :+: g) = D f :+: D g
  plug (L df, x) = L (plug (df, x))
  plug (R dg, x) = R (plug (dg, x))

instance (Differentiable f, Differentiable g) => Differentiable (f :*: g) where
  type D (f :*: g) = (D f :*: g) :+: (f :*: D g)
  plug (L (df :&: g), x) = plug (df, x) :&: g
  plug (R (f :&: dg), x) = f :&: plug (dg, x)

Actually, maybe it is relevant. If you're feeling adventurous, this unfinished article shows how to use Void to compress the representation of terms with free variables

data Term f x = Var x | Con (f (Term f x))   -- the Free monad, yet again

in any syntax generated freely from a Differentiable and Traversable functor f. We use Term f Void to represent regions with no free variables, and [D f (Term f Void)] to represent tubes tunnelling through regions with no free variables either to an isolated free variable, or to a junction in the paths to two or more free variables. Must finish that article sometime.

For a type with no values (or at least, none worth speaking of in polite company), Void is remarkably useful. And absurd is how you use it.

Solution 3

I'm thinking that perhaps it's useful in some cases as a type-safe way of exhaustively handling "can't happen" cases

This is precisely right.

You could say that absurd is no more useful than const (error "Impossible"). However, it is type restricted, so that its only input can be something of type Void, a data type which is intentionally left uninhabited. This means that there is no actual value that you can pass to absurd. If you ever end up in a branch of code where the type checker thinks that you have access to something of type Void, then, well, you are in an absurd situation. So you just use absurd to basically mark that this branch of code should never be reached.

"Ex falso quodlibet" literally means "from [a] false [proposition], anything follows". So when you find that you are holding a piece of data whose type is Void, you know you have false evidence in your hands. You can therefore fill any hole you want (via absurd), because from a false proposition, anything follows.

I wrote a blog post about the ideas behind Conduit which has an example of using absurd.

http://unknownparallel.wordpress.com/2012/07/30/pipes-to-conduits-part-6-leftovers/#running-a-pipeline

Solution 4

There are different ways how to represent the empty data type. One is an empty algebraic data type. Another way is to make it an alias for ∀α.α or

type Void' = forall a . a

in Haskell - this is how we can encode it in System F (see Chapter 11 of Proofs and Types). These two descriptions are of course isomorphic and the isomorphism is witnessed by \x -> x :: (forall a.a) -> Void and by absurd :: Void -> a.

In some cases, we prefer the explicit variant, usually if the empty data type appears in an argument of an function, or in a more complex data type, such as in Data.Conduit:

type Sink i m r = Pipe i i Void () m r

In some cases, we prefer the polymorphic variant, usually the empty data type is involved in the return type of a function.

absurd arises when we're converting between these two representations.

---

For example, callcc :: ((a -> m b) -> m a) -> m a uses (implicit) forall b. It could be as well of type ((a -> m Void) -> m a) -> m a, because a call to the contination doesn't actually return, it transfers control to another point. If we wanted to work with continuations, we could define

type Continuation r a = a -> Cont r Void

(We could use type Continuation' r a = forall b . a -> Cont r b but that'd require rank 2 types.) And then, vacuousM converts this Cont r Void into Cont r b.

(Also note that you can use haskellers.com to search for usage (reverse dependencies) of a certain package, like to see who and how uses the void package.)

Solution 5

Generally, you can use it to avoid apparently-partial pattern matches. For example, grabbing an approximation of the data type declarations from this answer:

data RuleSet a            = Known !a | Unknown String
data GoRuleChoices        = Japanese | Chinese
type LinesOfActionChoices = Void
type GoRuleSet            = RuleSet GoRuleChoices
type LinesOfActionRuleSet = RuleSet LinesOfActionChoices

Then you could use absurd like this, for example:

handleLOARules :: (String -> a) -> LinesOfActionsRuleSet -> a
handleLOARules f r = case r of
    Known   a -> absurd a
    Unknown s -> f s

View more solutions

Comments

[Artyom]

A quick search shows that the absurd function has been used in this article dealing with the Cont monad: haskellforall.com/2012/12/the-continuation-monad.html

[Daniel Wagner]

You can see absurd as one direction of the isomorphism between Void and forall a. a.

[Luis Casillas]

Huh, I can actually kinda follow that CPS bit. I'd certainly heard of the Curry-Howard double negation/CPS correspondences before, but not understood it; I'm not going to claim I fully get it now, but this certainly helps!

[Erik Kaplun]

"Life is a little bit hard, since Haskell is non strict" — what do you meant by that exactly?

[Cactus]

Would forall f. vacuous f = unsafeCoerce f be a valid GHC rewrite rule?

[dfeuer]

@Cactus, not really. Bogus Functor instances could be GADTs that aren't actually anything like functors.

[dfeuer]

@ErikAllik, in a strict language, Void is uninhabited. In Haskell, it contains _|_. In a strict language, a data constructor that takes an argument of type Void can never be applied, so the right hand side of the pattern match is unreachable. In Haskell, you need to use a ! to enforce that, and GHC probably won't notice that the path is unreachable.

[Cactus]

Would those Functors not break the fmap id = id rule? Or is that what you mean by "bogus" here?

[Erik Kaplun]

how about Agda? it's lazy but does it have _|_? and does it suffer from the same limitation then?

[Philip JF]

agda is, generally speaking, total and so the evaluation order is not observable. There is no closed agda term of the empty type unless you turn off the termination checker or something like that

[PyRulez]

@LuisCasillas The cool thing about CPS is it can encode classical logic. Exercise: Make something of type CPS (Either a (a -> Void)) (that is polymorphic in a.)

[Iceland_jack]

TypeApplications can be used to be more explicit about details of proof :: (forall a. a) -> Void: proof fls = fls @Void.

[jcalz]

@PyRulez could you give the answer to your exercise or some pointers to an answer? I've puzzled on it for a while and can't seem to come up with anything that works. I can't conjure up a magical value of type Either a (a -> Void) and pass it to the continuation, so if this is possible it presumably involves some recursive trick? Or maybe I'm way off. Any suggestions?

[PyRulez]

@jcalz hint: instead of finding something to pass to the argument, use it to construct a function of type a -> Void and a function of type (a -> Void) -> Void.

[jcalz]

@PyRulez thanks! The answer seems so obvious in retrospect that I can't see why I missed it beforehand.