¿Para qué sirve la función absurda en Data.Void?

La absurdfunción en Data.Voidtiene la siguiente firma, donde Voides el tipo lógicamente deshabitado exportado por ese paquete:

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

Sé suficiente lógica para obtener el comentario de la documentación de que esto corresponde, por la correspondencia de proposiciones como tipos, a la fórmula válida ⊥ → a.

De lo que estoy desconcertado y curioso es: ¿en qué tipo de problemas prácticos de programación es útil esta función? Estoy pensando que tal vez sea útil en algunos casos como una forma segura de manejar exhaustivamente los casos de "no puede suceder", pero no sé lo suficiente sobre los usos prácticos de Curry-Howard para saber si esa idea está en el camino correcto en absoluto.

EDITAR: Ejemplos preferiblemente en Haskell, pero si alguien quiere usar un lenguaje escrito de forma dependiente, no me voy a quejar ...

La vida es un poco dura, ya que Haskell no es estricto. El caso de uso general es manejar caminos imposibles. Por ejemplo

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

Esto resulta ser algo útil. Considere un tipo simple paraPipes

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

esta es una versión estricta y simplificada del tipo de tubería estándar de la Pipesbiblioteca de Gabriel Gonzales . Ahora, podemos codificar una tubería que nunca cede (es decir, un consumidor) como

type Consumer a r = Pipe a Void r

esto realmente nunca cede. La implicación de esto es que la regla de plegado adecuada para a Consumeres

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

o alternativamente, que puede ignorar el caso de rendimiento cuando se trata de consumidores. Esta es la versión general de este patrón de diseño: use tipos de datos polimórficos y Voidelimine las posibilidades cuando lo necesite.

Probablemente el uso más clásico de Voides en CPS.

type Continuation a = a -> Void

es decir, a Continuationes una función que nunca regresa. Continuationes la versión tipo de "no". De esto obtenemos una mónada de CPS (correspondiente a la lógica clásica)

newtype CPS a = Continuation (Continuation a)

dado que Haskell es puro, no podemos sacar nada de este tipo.

Considere esta representación para términos lambda parametrizados por sus variables libres. (Véanse los artículos de Bellegarde y Hook 1994, Bird y Paterson 1999, Altenkirch y Reus 1999.)

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

Ciertamente puede hacer que esto Functorcapture la noción de cambio de nombre y Monadcapture la noción de sustitución.

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

Ahora considere los términos cerrados : estos son los habitantes de Tm Void. Debería poder incrustar los términos cerrados en términos con variables libres arbitrarias. ¿Cómo?

fmap absurd :: Tm Void -> Tm a

El problema, por supuesto, es que esta función atravesará el término sin hacer nada precisamente. Pero es un toque más honesto que unsafeCoerce. Y es por eso que vacuousse agregó a Data.Void...

O escribe un evaluador. Aquí hay valores con variables libres en formato b.

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

Acabo de representar lambdas como cierres. El evaluador está parametrizado por un entorno que asigna variables libres aa valores superiores 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

Lo adivinaste. Para evaluar un plazo cerrado en cualquier objetivo

eval absurd :: Tm Void -> Val b

De manera más general, Voidrara vez se usa por sí solo, pero es útil cuando desea instanciar un parámetro de tipo de una manera que indique algún tipo de imposibilidad (por ejemplo, aquí, usando una variable libre en un término cerrado). A menudo, estos tipos parametrizadas vienen con funciones de orden superior operaciones de elevación de los parámetros a las operaciones en todo el tipo (por ejemplo, aquí, fmap, >>=, eval). Así que pasa absurdcomo la operación de propósito general Void.

Para otro ejemplo, imagínese usar Either e vpara capturar cálculos que con suerte le den un vpero podrían generar una excepción de tipo e. Puede utilizar este enfoque para documentar el riesgo de mal comportamiento de manera uniforme. Para cálculos que se comportan perfectamente en esta configuración, tómatelo ey Voidluego usa

either absurd id :: Either Void v -> v

para correr con seguridad o

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

para integrar componentes seguros en un mundo inseguro.

Ah, y un último hurra, manejar un "no puede suceder". Aparece en la construcción de cremallera genérica, en todos los lugares donde el cursor no puede estar.

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!

Decidí no borrar el resto, aunque no es exactamente relevante.

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)

De hecho, tal vez sea relevante. Si se siente aventurero, este artículo inacabado muestra cómo utilizar Voidpara comprimir la representación de términos con variables libres

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

en cualquier sintaxis generada libremente desde a Differentiabley Traversablefunctor f. Usamos Term f Voidpara representar regiones sin variables libres y [D f (Term f Void)]para representar tubos que hacen un túnel a través de regiones sin variables libres, ya sea a una variable libre aislada o a una unión en las rutas a dos o más variables libres. Debo terminar ese artículo en algún momento.

Para un tipo sin valores (o al menos, ninguno de los que valga la pena hablar en compañía cortés), Voides muy útil. Y así absurdes como lo usas.

Creo que tal vez sea útil en algunos casos como una forma segura de manejar de manera exhaustiva los casos de "no puede suceder"

Esto es precisamente correcto.

Se podría decir que absurdno es más útil que const (error "Impossible"). Sin embargo, tiene restricción de tipo, por lo que su única entrada puede ser algo de tipo Void, un tipo de datos que se deja intencionalmente deshabitado. Esto significa que no hay un valor real al que pueda pasar absurd. Si alguna vez terminas en una rama de código donde el verificador de tipos cree que tienes acceso a algo de tipo Void, entonces, bueno, estás en una situación absurda . Por lo tanto, solo usa absurdpara marcar básicamente que nunca se debe llegar a esta rama de código.

"Ex falso quodlibet" significa literalmente "de [una] falsa [proposición], todo sigue". Entonces, cuando descubre que tiene un dato cuyo tipo es Void, sabe que tiene pruebas falsas en sus manos. Por lo tanto, puede llenar cualquier hueco que desee (vía absurd), porque de una proposición falsa, todo se sigue.

Escribí una publicación de blog sobre las ideas detrás de Conduit que tiene un ejemplo de uso absurd.

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

Generalmente, puede usarlo para evitar coincidencias de patrones aparentemente parciales. Por ejemplo, tomando una aproximación de las declaraciones de tipo de datos de esta respuesta :

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

Entonces podrías usar absurdasí, por ejemplo:

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

Hay diferentes formas de representar el tipo de datos vacío . Uno es un tipo de datos algebraicos vacío. Otra forma es convertirlo en un alias para ∀α.α o

type Void' = forall a . a

en Haskell: así es como podemos codificarlo en el Sistema F (consulte el Capítulo 11 de Pruebas y tipos ). Estas dos descripciones son, por supuesto isomorfo y el isomorfismo se evidencia con \x -> x :: (forall a.a) -> Voidy absurd :: Void -> a.

En algunos casos, preferimos la variante explícita, generalmente si el tipo de datos vacío aparece en un argumento de una función, o en un tipo de datos más complejo, como en Data.Conduit :

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

En algunos casos, preferimos la variante polimórfica, generalmente el tipo de datos vacío está involucrado en el tipo de retorno de una función.

absurd surge cuando estamos convirtiendo entre estas dos representaciones.

Por ejemplo, callcc :: ((a -> m b) -> m a) -> m ausa (implícito) forall b. También podría ser de tipo ((a -> m Void) -> m a) -> m a, porque una llamada a la continuación en realidad no regresa, transfiere el control a otro punto. Si quisiéramos trabajar con continuaciones, podríamos definir

type Continuation r a = a -> Cont r Void

(Podríamos usar, type Continuation' r a = forall b . a -> Cont r bpero eso requeriría tipos de rango 2). Y luego, vacuousMconvierte esto Cont r Voiden Cont r b.

(También tenga en cuenta que puede usar haskellers.com para buscar el uso (dependencias inversas) de un determinado paquete, como para ver quién y cómo usa el paquete void ).

En lenguajes de tipo dependiente como Idris, probablemente sea más útil que en Haskell. Por lo general, en una función total, cuando el patrón coincide con un valor que en realidad no se puede introducir en la función, entonces construye un valor de tipo deshabitado y lo usa absurdpara finalizar la definición del caso.

Por ejemplo, esta función elimina un elemento de una lista con la restricción de tipo de nivel que está presente allí:

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

Donde el segundo caso dice que hay un determinado elemento en una lista vacía, lo cual es, bueno, absurdo. En general, sin embargo, el compilador no sabe esto y, a menudo, tenemos que ser explícitos. Luego, el compilador puede verificar que la definición de la función no sea parcial y obtenemos mayores garantías en tiempo de compilación.

A través del punto de vista de Curry-Howard, donde hay proposiciones, entonces absurdes una especie de QED en una prueba por contradicción.