What's the absurd function in Data.Void useful

问题:

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

回答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.

回答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.

回答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

回答4:

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

回答5:

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

回答6:

In dependently-typed languages like Idris, it's probably more useful than in Haskell. Typically, in a total function when you pattern match a value that actually cannot be shoved into the function, you would then construct a value of uninhabited type and use absurd to finalize the case definition.

For example this function removes an element from a list with the type-level costraint that it's present there:

shrink : (xs : Vect (S n) a) -> Elem x xs -> Vect n a
shrink (x :: ys) Here = ys
shrink (y :: []) (There p) = absurd p
shrink (y :: (x :: xs)) (There p) = y :: shrink (x :: xs) p

Where the second case is saying that there is an certain element in an empty list, which is, well absurd. In general, however, the compiler does not know this and we often have to be explicit. Then the compiler can check that the function definition is not partial and we obtain stronger compile-time guarantees.

Through Curry-Howard point of view, where are propositions, then absurd is sort of the QED in a proof by contradiction.