haskell - ¿Para qué sirve la función absurda en Data.Void?
type-theory curry-howard (6)
Estoy pensando que tal vez sea útil en algunos casos como una forma segura de tipo para manejar exhaustivamente los casos de "no puede suceder"
Esto es precisamente correcto.
Se podría decir que absurd no es más útil que const (error "Impossible") . Sin embargo, es de tipo restringido, por lo que su única entrada puede ser algo del tipo Void , un tipo de datos que se deja intencionalmente deshabitado. Esto significa que no hay un valor real que pueda pasar al absurd . Si alguna vez terminas en una rama de código donde el verificador de tipos piensa que tienes acceso a algo del tipo Void , entonces, bueno, estás en una situación absurda . Entonces, simplemente usa el absurd para marcar que esta rama del código nunca debería ser alcanzada.
"Ex falso quodlibet" literalmente significa "de [a] falso [proposición], todo sigue". Entonces, cuando descubre que está reteniendo un dato cuyo tipo es Void , sabe que tiene pruebas falsas en sus manos. Por lo tanto, puede llenar cualquier agujero que desee (a través del absurd ), porque de una proposición falsa, todo sigue.
Escribí una publicación en el blog sobre las ideas detrás de Conduit que tiene un ejemplo de uso del absurd .
La función absurd en Data.Void tiene la siguiente firma, donde Void es 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 la observación de la documentación de que esto corresponde, por la correspondencia de proposiciones como tipos, a la fórmula válida ⊥ → a .
Lo que me deja perplejo y curioso es: ¿en qué tipo de problemas de programación práctica es útil esta función? Estoy pensando que tal vez sea útil en algunos casos como una forma segura de tipo para manejar exhaustivamente los casos de "no puede suceder", pero no sé lo suficiente sobre los usos prácticos de Curry-Howard para decir si esa idea está en el la pista correcta en absoluto.
EDITAR: Ejemplos preferiblemente en Haskell, pero si alguien quiere usar un lenguaje dependiente, no me voy a quejar ...
Considere esta representación para términos lambda parametrizados por sus variables libres. (Véanse los documentos 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 puedes hacer de esto un Functor , capturando la noción de cambio de nombre, y una Monad capturando 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 insertar los términos cerrados en términos con variables libres arbitrarias. ¿Cómo?
fmap absurd :: Tm Void -> Tm a
La atrapada, por supuesto, es que esta función atravesará el término haciendo precisamente nada. Pero es un toque más honesto que unsafeCoerce . Y es por eso que Data.Void fue agregado a Data.Void ...
O escribe un evaluador. Aquí hay valores con variables libres en 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 se parametriza mediante un entorno mapeando variables libres en a a valores sobre 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 término cerrado en cualquier objetivo
eval absurd :: Tm Void -> Val b
De manera más general, Void rara vez se usa solo, pero es útil cuando se quiere crear una instancia de 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 parametrizados vienen con funciones de orden superior que levantan operaciones sobre los parámetros para operaciones en todo el tipo (por ejemplo, aquí, fmap , >>= , eval ). Entonces pasas absurd como la operación de propósito general en Void .
Para otro ejemplo, imagine usar Either ev para capturar cálculos que, con suerte, le den una v pero que podrían generar una excepción de tipo e . Puede utilizar este enfoque para documentar el riesgo de mal comportamiento de manera uniforme. Para realizar cálculos perfectamente correctos en esta configuración, tome e para ser Void , luego use
either absurd id :: Either Void v -> v
para correr de forma segura o
either absurd Right :: Either Void v -> Either e v
para incrustar componentes seguros en un mundo inseguro.
Ah, y un último hurra, manejando un "no puede suceder". Aparece en la construcción genérica de la cremallera, en todas partes 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 eliminar el resto, a pesar de que 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)
En realidad, tal vez sea relevante. Si te sientes aventurero, este artículo inacabado muestra cómo usar Void para comprimir la representación de términos con variables gratuitas
data Term f x = Var x | Con (f (Term f x)) -- the Free monad, yet again
en cualquier sintaxis generada libremente desde un funcionador Differentiable y Traversable f . Utilizamos Term f Void para representar regiones sin variables libres, y [D f (Term f Void)] para representar los túneles de túneles a través de regiones sin variables libres a una variable libre aislada, o a una unión en las rutas a dos o más variables gratuitas Debe terminar ese artículo en algún momento.
Para un tipo sin valores (o al menos, ninguno de los que vale la pena mencionar en compañía cortés), Void es notablemente útil. Y absurd es cómo lo usas.
En general, 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 absurd como este, por ejemplo:
handleLOARules :: (String -> a) -> LinesOfActionsRuleSet -> a
handleLOARules f r = case r of
Known a -> absurd a
Unknown s -> f s
En idiomas de tipo dependiente como Idris, es probablemente más útil que en Haskell. Normalmente, en una función total cuando el patrón coincide con un valor que en realidad no puede insertarse en la función, entonces construiría un valor de tipo deshabitado y usaría absurd para finalizar la definición del caso.
Por ejemplo, esta función elimina un elemento de una lista con el tipo de coste costraint 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 cierto elemento en una lista vacía, que es, así, absurdo. En general, sin embargo, el compilador no lo sabe y, a menudo, tenemos que ser explícitos. Entonces el compilador puede verificar que la definición de la función no es parcial y obtenemos garantías de tiempo de compilación más fuertes.
A través del punto de vista de Curry-Howard, dónde están las proposiciones, entonces absurd es una especie de QED en una prueba por contradicción.
Hay diferentes formas de representar el tipo de datos vacío . Uno es un tipo de datos algebraicos vacíos. 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 (ver el Capítulo 11 de Pruebas y Tipos ). Estas dos descripciones son por supuesto isomórficas y el isomorfismo es atestiguado por /x -> x :: (forall aa) -> Void y por 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 devolución de una función.
absurd surge cuando estamos convirtiendo entre estas dos representaciones.
Por ejemplo, callcc :: ((a -> mb) -> ma) -> ma usa (implícito) forall b . Podría ser también de tipo ((a -> m Void) -> ma) -> ma , porque una llamada a la continación en realidad no regresa, sino que 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 el type Continuation'' ra = forall b . a -> Cont rb pero eso requeriría el rango 2 tipos.) Y luego, vacuousM convierte este Cont r Void en Cont rb .
(También tenga en cuenta que puede usar haskellers.com para buscar el uso (dependencias inversas) de un determinado paquete, como ver quién y cómo utiliza el paquete nulo ).
La vida es un poco difícil, 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 para Pipes
data Pipe a b r
= Pure r
| Await (a -> Pipe a b r)
| Yield !b (Pipe a b r)
esta es una versión simplificada y estricta del tipo de cañería estándar de la biblioteca Pipes de Gabriel Gonzales. Ahora, podemos codificar una tubería que nunca rinde (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 doblez adecuada para un Consumer es
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 trata con consumidores. Esta es la versión general de este patrón de diseño: utilice tipos de datos polimórficos y Void para deshacerse de las posibilidades cuando lo necesite.
Probablemente el uso más clásico de Void es en CPS.
type Continuation a = a -> Void
es decir, una Continuation es una función que nunca regresa. Continuation es 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)
ya que Haskell es puro, no podemos sacar nada de este tipo.