Para que serve a função absurda em Data.Void?

A absurdfunção in Data.Voidtem a seguinte assinatura, onde Voidé o tipo logicamente inabitado exportado por esse pacote:

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

Eu conheço lógica suficiente para obter a observação da documentação de que isso corresponde, pela correspondência proposições como tipos, à fórmula válida ⊥ → a.

O que estou intrigado e curioso é: em que tipo de problemas práticos de programação essa função é útil? Estou pensando que talvez seja útil em alguns casos como uma forma segura de lidar exaustivamente com casos "não podem acontecer", mas não sei o suficiente sobre os usos práticos de Curry-Howard para dizer se essa ideia está no caminho certo em tudo.

EDITAR: Exemplos de preferência em Haskell, mas se alguém quiser usar uma linguagem de digitação dependente, não vou reclamar ...

A vida é um pouco difícil, já que Haskell não é rigoroso. O caso de uso geral é lidar com caminhos impossíveis. Por exemplo

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

Isso acabou sendo um tanto útil. Considere um tipo simples paraPipes

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

esta é uma versão estrita e simplificada do tipo de tubos padrão da Pipesbiblioteca de Gabriel Gonzales . Agora, podemos codificar um tubo que nunca cede (ou seja, um consumidor) como

type Consumer a r = Pipe a Void r

isso realmente nunca cede. A implicação disso é que a regra de dobra adequada para a Consumeré

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

ou alternativamente, que você pode ignorar o caso de rendimento ao lidar com os consumidores. Esta é a versão geral deste padrão de projeto: use tipos de dados polimórficos e Voidse livre das possibilidades quando precisar.

Provavelmente, o uso mais clássico de Voidé no CPS.

type Continuation a = a -> Void

ou seja, a Continuationé uma função que nunca retorna. Continuationé a versão do tipo de "não". A partir disso, obtemos uma mônada de CPS (correspondente à lógica clássica)

newtype CPS a = Continuation (Continuation a)

como Haskell é puro, não podemos obter nada desse tipo.

Considere esta representação para termos lambda parametrizados por suas variáveis ​​livres. (Ver artigos de Bellegarde e Hook 1994, Bird e Paterson 1999, Altenkirch e Reus 1999.)

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

Você certamente pode tornar isso um Functor, capturando a noção de renomeação e Monadcapturando a noção de substituição.

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

Agora considere os termos fechados : estes são os habitantes de Tm Void. Você deve ser capaz de incorporar os termos fechados em termos com variáveis ​​livres arbitrárias. Quão?

fmap absurd :: Tm Void -> Tm a

O problema, é claro, é que essa função atravessará o termo sem fazer exatamente nada. Mas é um pouco mais honesto do que unsafeCoerce. E é por isso que vacuousfoi adicionado a Data.Void...

Ou escreva um avaliador. Aqui estão os valores com variáveis ​​livres em b.

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

Acabei de representar lambdas como encerramentos. O avaliador é parametrizado por um ambiente que mapeia variáveis ​​livres em avalores 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

Você adivinhou. Para avaliar um termo fechado em qualquer alvo

eval absurd :: Tm Void -> Val b

De modo mais geral, Voidraramente é usado sozinho, mas é útil quando você deseja instanciar um parâmetro de tipo de uma forma que indica algum tipo de impossibilidade (por exemplo, aqui, usando uma variável livre em um termo fechado). Muitas vezes, estes tipos parametrizados vêm com funções de ordem superior operações de elevação sobre os parâmetros para as operações em todo o tipo (por exemplo, aqui, fmap, >>=, eval). Então você passa absurdcomo a operação de propósito geral Void.

Para outro exemplo, imagine usar Either e vpara capturar cálculos que, felizmente, fornecem um, vmas podem gerar uma exceção de tipo e. Você pode usar essa abordagem para documentar o risco de mau comportamento de maneira uniforme. Para cálculos perfeitamente bem comportados nesta configuração, tome ecomo e Void, em seguida, use

either absurd id :: Either Void v -> v

para correr com segurança ou

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

para incorporar componentes seguros em um mundo inseguro.

Ah, e um último viva, lidar com um "não pode acontecer". Ele aparece na construção genérica do zíper, em todos os lugares onde o cursor não pode 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!

Decidi não excluir o resto, embora não seja exatamente 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)

Na verdade, talvez seja relevante. Se você está se sentindo aventureiro, este artigo inacabado mostra como Voidcompactar a representação de termos com variáveis ​​livres

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

em qualquer sintaxe gerada livremente a partir de um Differentiablee Traversablefunctor f. Usamos Term f Voidpara representar regiões sem variáveis ​​livres e [D f (Term f Void)]para representar tubos tunelando através de regiões sem variáveis ​​livres para uma variável livre isolada, ou para uma junção nos caminhos para duas ou mais variáveis ​​livres. Devo terminar esse artigo algum dia.

Para um tipo sem valores (ou, pelo menos, nenhum que valha a pena falar em companhia educada), Voidé extremamente útil. E absurdé assim que você o usa.

Estou pensando que talvez seja útil em alguns casos como uma forma segura de lidar exaustivamente com casos "não pode acontecer"

Isso é precisamente correto.

Você poderia dizer que absurdnão é mais útil do que const (error "Impossible"). No entanto, ele é restrito ao tipo, de modo que sua única entrada pode ser algo do tipo Void, um tipo de dados que é intencionalmente deixado inabitado. Isso significa que não há nenhum valor real para o qual você possa passar absurd. Se você alguma vez acabar em um ramo de código onde o verificador de tipo pensa que você tem acesso a algo do tipo Void, então, bem, você está em uma situação absurda . Então, você apenas usa absurdpara basicamente marcar que esse ramo do código nunca deve ser alcançado.

"Ex falso quodlibet" significa literalmente "de [uma] falsa [proposição], segue-se qualquer coisa". Portanto, quando você descobrir que está segurando um dado cujo tipo é Void, você sabe que tem evidências falsas em suas mãos. Você pode, portanto, preencher qualquer lacuna que quiser (via absurd), porque de uma proposição falsa, tudo se segue.

Eu escrevi uma postagem no blog sobre as ideias por trás do Conduit que tem um exemplo de uso absurd.

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

Geralmente, você pode usá-lo para evitar correspondências de padrões aparentemente parciais. Por exemplo, pegando uma aproximação das declarações de tipo de dados desta resposta :

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

Então você poderia usar absurdassim, por exemplo:

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

Existem diferentes maneiras de representar o tipo de dados vazio . Um é um tipo de dados algébrico vazio. Outra maneira é torná-lo um alias para ∀α.α ou

type Void' = forall a . a

em Haskell - é assim que podemos codificá-lo no Sistema F (consulte o Capítulo 11 de Provas e tipos ). Essas duas descrições são obviamente isomórficas e o isomorfismo é testemunhado por \x -> x :: (forall a.a) -> Voide por absurd :: Void -> a.

Em alguns casos, preferimos a variante explícita, geralmente se o tipo de dados vazio aparece em um argumento de uma função, ou em um tipo de dados mais complexo, como em Data.Conduit :

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

Em alguns casos, preferimos a variante polimórfica, geralmente o tipo de dados vazio está envolvido no tipo de retorno de uma função.

absurd surge quando estamos convertendo entre essas duas representações.

Por exemplo, callcc :: ((a -> m b) -> m a) -> m ausa (implícito) forall b. Também poderia ser do tipo ((a -> m Void) -> m a) -> m a, porque uma chamada para a continação não retorna realmente, ela transfere o controle para outro ponto. Se quiséssemos trabalhar com continuações, poderíamos definir

type Continuation r a = a -> Cont r Void

(Poderíamos usar, type Continuation' r a = forall b . a -> Cont r bmas isso exigiria tipos de classificação 2.) E então, vacuousMconverte isso Cont r Voidem Cont r b.

(Observe também que você pode usar haskellers.com para pesquisar o uso (dependências reversas) de um determinado pacote, como para ver quem e como usa o pacote void .)

Em linguagens com tipos dependentes como Idris, é provavelmente mais útil do que em Haskell. Normalmente, em uma função total, quando você padroniza a correspondência de um valor que realmente não pode ser empurrado para a função, você construiria um valor do tipo não habitado e utilizaria absurdpara finalizar a definição de caso.

Por exemplo, esta função remove um elemento de uma lista com a restrição de nível de tipo que está presente lá:

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

Onde o segundo caso é dizer que existe um certo elemento em uma lista vazia, o que é, bem absurdo. Em geral, entretanto, o compilador não sabe disso e muitas vezes temos que ser explícitos. Então, o compilador pode verificar se a definição da função não é parcial e obter garantias de tempo de compilação mais fortes.

Do ponto de vista de Curry-Howard, onde estão as proposições, então absurdé uma espécie de QED em uma prova por contradição.