Ce qui est absurde, en fonction des Données.Void utile?

Question

L' absurd fonction Data.Void a la signature suivante, où Void est logiquement inhabitée type exportés par ce package:

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

Je sais assez logique pour obtenir la documentation la remarque que cela correspond, par les propositions-comme-les types de correspondance, à la validité de la formule ⊥ → a.

Ce que je suis perplexe et curieux de savoir: dans ce genre de pratique, les problèmes de programmation est cette fonction utile? Je pense que c'est peut-être utile dans certains cas comme un moyen sûr de manière exhaustive la manipulation "ne peut pas se produire", mais je ne sais pas assez sur les utilisations pratiques de Curry-Howard à dire si cette idée est sur la bonne voie.

EDIT: Exemples de préférence en Haskell, mais si quelqu'un veut utiliser un dépendante tapé langue que je ne vais pas me plaindre...

Answer 1

Considérer cette représentation pour lambda termes paramétrés par leurs variables libres. (Voir les documents par Bellegarde et Crochet de 1994, d'Oiseaux et de Paterson 1999, Altenkirch et Reus 1999.)

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

Vous pouvez certainement faire de cette un Functor, saisir la notion de changement de nom et un Monad saisir la notion de 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))

Considérons maintenant le fermé termes: ce sont les habitants de Tm Void. Vous devriez être en mesure d'intégrer la fermé termes en termes arbitraire de variables libres. Comment?

fmap absurd :: Tm Void -> Tm a

Le hic, bien sûr, est que cette fonction va parcourir le terme fait rien de précis. Mais c'est un peu plus honnête que d' unsafeCoerce. Et c'est pourquoi, vacuous a été ajouté à l' Data.Void...

Ou écrire un évaluateur. Voici les valeurs, avec 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

J'ai simplement représenté lambdas que les fermetures. L'évaluateur est paramétrisée par un environnement de mappage de variables libres en a pour des valeurs en 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

Vous l'aurez deviné. Pour évaluer une période fermée à toute cible

eval absurd :: Tm Void -> Val b

Plus généralement, Void est rarement utilisé seul, mais il est pratique lorsque vous souhaitez instancier un paramètre de type dans une manière qui indique une sorte d'impossibilité (par exemple, ici, à utiliser une variable dans une période fermée). Souvent, ces types paramétrés viennent avec des fonctions d'ordre supérieur opérations de levage sur les paramètres des opérations sur tout type (par exemple, ici, fmap, >>=, eval). Si vous passez absurd comme l'opération sur Void.

Pour un autre exemple, imaginez l'aide d' Either e v pour capturer les calculs qui nous l'espérons vous donner un v mais peut soulever une exception de type e. Vous pouvez utiliser cette approche pour le document risque de mal se comporter de manière uniforme. Pour parfaitement bien comportés les calculs dans ce cadre, prendre en e être Void, puis utilisez

either absurd id :: Either Void v -> v

pour exécuter en toute sécurité ou

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

pour intégrer des composants de sécurité dans un monde dangereux.

Oh, et un dernier tour de piste, la manipulation d'un "ne peut pas se produire". Il apparaît dans le générique de fermeture à glissière de la construction, de partout que le curseur ne peut pas être.

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!

J'ai décidé de ne pas supprimer le reste, même si elle n'est pas pertinente.

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 fait, c'est peut-être pertinente. Si vous vous sentez aventureux, ce inachevé article montre comment utiliser Void pour compresser la représentation des termes avec variables libres

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

dans toute la syntaxe générée librement à partir d'un Differentiable et Traversable foncteur f. Nous utilisons Term f Void pour représenter les régions avec variables libres, et [D f (Term f Void)] pour représenter des tubes de tunnels à travers des régions avec pas de variables libres, soit à un cas isolé gratuit variable, ou à un point de jonction dans les chemins de deux ou plusieurs variables libres. Doit terminer cet article de temps en temps.

Pour un type sans valeurs (ou du moins n'en vaut parler de dans la bonne société), Void est remarquablement utile. Et absurd est la façon dont vous l'utiliser.

Answer 2

La vie est un peu dur, car Haskell est non stricte. Le général de cas d'utilisation est de gérer impossible chemins. Par exemple

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

Cela s'avère être quelque chose d'utile. Considérons un type simple pour Pipes

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

c'est un strict identifiés et version simplifiée de la norme tuyaux type de Gabriel Gonzales' Pipes bibliothèque. Maintenant, nous pouvons coder un tuyau qui n'a jamais rendements (par exemple, un consommateur)

type Consumer a r = Pipe a Void r

cela n'a jamais vraiment rendements. La conséquence de cela est que le bon pli règle pour un Consumer est

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 sinon, que vous pouvez ignorer le rendement des cas lors de l'affaire avec les consommateurs. C'est la version de ce modèle de conception: utilisation polymorphes types de données et d' Void pour se débarrasser de possibilités lorsque vous en avez besoin.

Sans doute le plus classique de l'utilisation de Void est dans le CPS.

type Continuation a = a -> Void

c'est, Continuation est une fonction qui ne retourne jamais. Continuation est le type de version de "non." De là, nous obtenons une monade de CPS (correspondant à la logique classique)

newtype CPS a = Continuation (Continuation a)

depuis Haskell est pur, nous ne pouvons pas obtenir quoi que ce soit de ce type.

Answer 3

Je pense que c'est peut-être utile dans certains cas comme un moyen sûr de manière exhaustive la manipulation "ne peut pas se produire" des cas

C'est précisément pour cette raison.

On pourrait dire que l' absurd n'est pas plus utile qu' const (error "Impossible"). Cependant, il est de type restreint, de sorte que sa seule entrée peut être quelque chose de type Void, un type de données qui est intentionnellement laissée en inhabitée. Cela signifie qu'il n'y a pas de réelle valeur que vous pouvez passer à l' absurd. Si jamais vous retrouver dans une branche de code où le type checker pense que vous avez accès à quelque chose de type Void, alors, eh bien, vous êtes dans l' absurde de la situation. Donc, il vous suffit d'utiliser absurd en gros de marque de cette branche de code ne doit jamais être atteint.

"Ex falso quodlibet" signifie littéralement "de [a] faux [proposition], tout ce qui suit". Ainsi, lorsque vous trouvez que vous êtes en tenant un morceau de données dont le type est - Void, vous savez que vous avez de fausses preuves dans vos mains. Vous pouvez donc remplir toutes les trou que vous voulez (par absurd), en raison d'une fausse proposition, tout ce qui suit.

J'ai écrit un billet de blog sur les idées derrière le Conduit qui est un exemple de l'utilisation de absurd.

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

Answer 4

Généralement, vous pouvez l'utiliser pour éviter apparemment partielle modèle correspond. Par exemple, en saisissant une approximation du type de données des déclarations de cette réponse:

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

Ensuite, vous pouvez utiliser absurd comme ceci, par exemple:

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

Answer 5

Il y a différentes manières de représenter le vide type de données. L'un est vide algébrique de type de données. Une autre façon est d'en faire un alias pour ∀α.α ou

type Void' = forall a . a

en Haskell - c'est la façon dont nous pouvons encoder dans le Système F (voir le Chapitre 11 de Preuves et de Types). Ces deux descriptions sont naturellement isomorphe et l'isomorphisme est assisté par des \x -> x :: (forall a.a) -> Void et en absurd :: Void -> a.

Dans certains cas, nous préférons l'explicite variante, d'habitude, si le vide type de données apparaît dans un argument d'une fonction, ou dans un complexe de type de données, comme dans les Données.Conduit:

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

Dans certains cas, nous préférons le polymorphe variante, généralement le vide type de données est impliqué dans le type de retour d'une fonction.

absurd se pose lorsque nous sommes conversion entre ces deux représentations.

---

Par exemple, callcc :: ((a -> m b) -> m a) -> m a utilise (implicite) forall b. Il pourrait être aussi bien de type ((a -> m Void) -> m a) -> m a, en raison d'un appel à la contination ne fait pas de retour, il transfère le contrôle à un autre point. Si nous avons voulu travailler avec les suites, on pourrait définir l'

type Continuation r a = a -> Cont r Void

(Nous pourrions utiliser type Continuation' r a = forall b . a -> Cont r b , mais que j'avais besoin rang 2 types.) Et puis, vacuousM le convertit en Cont r Void en Cont r b.

(Notez également que vous pouvez utiliser haskellers.com de recherche pour l'utilisation (dépendances inverses) pour certains paquets, comme pour voir qui et comment utilise le vide paquet.)