À quoi sert la fonction absurde de Data.Void?

La absurdfonction dans Data.Voida la signature suivante, où Voidest le type logiquement inhabité exporté par ce package:

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

Je connais assez de logique pour obtenir la remarque de la documentation que cela correspond, par la correspondance des propositions en tant que types, à la formule valide ⊥ → a.

Ce qui me rend perplexe et curieux, c'est: dans quel genre de problèmes de programmation pratiques cette fonction est-elle utile? Je pense que c'est peut-être utile dans certains cas en tant que moyen sûr de traiter de manière exhaustive les cas "impossible à réaliser", mais je n'en sais pas assez sur les utilisations pratiques de Curry-Howard pour dire si cette idée est sur le bonne voie du tout.

EDIT: Exemples de préférence en Haskell, mais si quelqu'un veut utiliser un langage typé de manière dépendante, je ne vais pas me plaindre ...

La vie est un peu dure, puisque Haskell n'est pas strict. Le cas d'utilisation général est de gérer les chemins impossibles. Par exemple

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

Cela s'avère quelque peu utile. Considérez un type simple pourPipes

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

il s'agit d'une version stricte et simplifiée du type de tuyaux standard de la Pipesbibliothèque de Gabriel Gonzales . Maintenant, nous pouvons encoder un tube qui ne cède jamais (c'est-à-dire un consommateur) comme

type Consumer a r = Pipe a Void r

cela ne cède vraiment jamais. L'implication de ceci est que la règle de pliage appropriée pour a Consumerest

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 bien, que vous pouvez ignorer le cas de rendement lorsque vous traitez avec les consommateurs. C'est la version générale de ce modèle de conception: utilisez des types de données polymorphes et Voidéliminez les possibilités lorsque vous en avez besoin.

L'utilisation la plus classique de Voidest probablement dans CPS.

type Continuation a = a -> Void

autrement dit, a Continuationest une fonction qui ne revient jamais. Continuationest la version type de «non». De cela, nous obtenons une monade de CPS (correspondant à la logique classique)

newtype CPS a = Continuation (Continuation a)

puisque Haskell est pur, nous ne pouvons rien obtenir de ce type.

Considérez cette représentation pour les termes lambda paramétrés par leurs variables libres. (Voir les articles de Bellegarde et Hook 1994, Bird et Paterson 1999, Altenkirch et Reus 1999.)

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

Vous pouvez certainement en faire un Functor, capturer la notion de changement de nom et Monadcapturer 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 les termes fermés : ce sont les habitants de Tm Void. Vous devriez pouvoir intégrer les termes fermés dans des termes avec des variables libres arbitraires. Comment?

fmap absurd :: Tm Void -> Tm a

Le hic, bien sûr, est que cette fonction traversera le terme sans rien faire. Mais c'est une touche plus honnête que unsafeCoerce. Et c'est pourquoi a vacuousété ajouté à Data.Void...

Ou écrivez un évaluateur. Voici les valeurs avec des variables libres dans b.

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

Je viens de représenter les lambdas comme des fermetures. L'évaluateur est paramétré par un environnement mappant les variables libres avers les valeurs 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

Tu l'as deviné. Pour évaluer un terme fermé à n'importe quelle cible

eval absurd :: Tm Void -> Val b

Plus généralement, Voidest rarement utilisé seul, mais est pratique lorsque vous voulez instancier un paramètre de type d'une manière qui indique une sorte d'impossibilité (par exemple, ici, en utilisant une variable libre dans un terme fermé). Souvent , ces types paramétrés viennent avec des fonctions d'ordre supérieur des opérations de levage sur les paramètres des opérations du type entier (par exemple, ici, fmap, >>=, eval). Vous passez donc absurdcomme opération à usage général Void.

Pour un autre exemple, imaginez utiliser Either e vpour capturer des calculs qui, espérons-le, vous donneront un vmais pourraient soulever une exception de type e. Vous pouvez utiliser cette approche pour documenter uniformément le risque de mauvais comportement. Pour des calculs parfaitement bien comportés dans ce cadre, prenez epour être Void, puis utilisez

either absurd id :: Either Void v -> v

pour courir en toute sécurité ou

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

pour intégrer des composants sûrs dans un monde dangereux.

Oh, et un dernier hourra, gérer un "impossible". Il apparaît dans la construction générique de la fermeture à glissière, partout où 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 ce n'est pas tout à fait pertinent.

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 pertinent. Si vous vous sentez aventureux, cet article inachevé montre comment utiliser Voidpour compresser la représentation des termes avec des variables libres

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

dans n'importe quelle syntaxe générée librement à partir d'un foncteur Differentiableet . Nous utilisons pour représenter des régions sans variables libres et pour représenter des tubes qui traversent des régions sans variables libres, soit vers une variable libre isolée, soit vers une jonction dans les chemins vers deux ou plusieurs variables libres. Doit finir cet article un jour.TraversablefTerm f Void[D f (Term f Void)]

Pour un type sans valeurs (ou du moins, aucune digne de parler en compagnie polie), Voidest remarquablement utile. Et absurdc'est comment vous l'utilisez.

Je pense que c'est peut-être utile dans certains cas en tant que moyen sûr de gérer de manière exhaustive les cas «impossible»

C'est exactement vrai.

Vous pourriez dire que ce absurdn'est pas plus utile que 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é inhabité. Cela signifie qu'il n'y a pas de valeur réelle à laquelle vous pouvez passer absurd. Si jamais vous vous retrouvez dans une branche de code où le vérificateur de type pense que vous avez accès à quelque chose de type Void, alors, eh bien, vous êtes dans une situation absurde . Donc, vous utilisez simplement absurdpour marquer que cette branche de code ne doit jamais être atteinte.

«Ex falso quodlibet» signifie littéralement «à partir [d'une] fausse [proposition], tout suit». Ainsi, lorsque vous constatez que vous détenez une donnée dont le type est Void, vous savez que vous avez entre les mains de fausses preuves. Vous pouvez donc remplir n'importe quel trou que vous voulez (via absurd), car à partir d'une fausse proposition, tout suit.

J'ai écrit un article de blog sur les idées derrière Conduit qui a un exemple d'utilisation absurd.

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

Généralement, vous pouvez l'utiliser pour éviter les correspondances de motifs apparemment partielles. Par exemple, saisir une approximation des déclarations de type de données à partir 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 absurdcomme ceci, par exemple:

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

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

type Void' = forall a . a

dans Haskell - c'est ainsi que nous pouvons l'encoder dans le système F (voir le chapitre 11 des preuves et types ). Ces deux descriptions sont bien sûr isomorphes et l'isomorphisme est observé par \x -> x :: (forall a.a) -> Voidet par absurd :: Void -> a.

Dans certains cas, nous préférons la variante explicite, généralement si le type de données vide apparaît dans un argument d'une fonction, ou dans un type de données plus complexe, comme dans Data.Conduit :

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

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

absurd se produit lorsque nous convertissons entre ces deux représentations.

Par exemple, callcc :: ((a -> m b) -> m a) -> m auses (implicite) forall b. Cela peut aussi être de type ((a -> m Void) -> m a) -> m a, car un appel à la contination ne revient pas réellement, il transfère le contrôle à un autre point. Si nous voulions travailler avec des suites, nous pourrions définir

type Continuation r a = a -> Cont r Void

(Nous pourrions utiliser type Continuation' r a = forall b . a -> Cont r bmais cela nécessiterait des types de rang 2.) Et puis, vacuousMconvertit cela Cont r Voiden Cont r b.

(Notez également que vous pouvez utiliser haskellers.com pour rechercher l'utilisation (dépendances inversées) d'un certain package, comme pour voir qui et comment utilise le package void .)

Dans les langages à typage dépendant comme Idris, c'est probablement plus utile que dans Haskell. En règle générale, dans une fonction totale, lorsque le modèle correspond à une valeur qui ne peut pas être déplacée dans la fonction, vous construisez alors une valeur de type inhabité et utilisez absurdpour finaliser la définition de cas.

Par exemple, cette fonction supprime un élément d'une liste avec la contrainte de coût au niveau du type qui y est présente:

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

Où le second cas dit qu'il y a un certain élément dans une liste vide, ce qui est bien absurde. En général, cependant, le compilateur ne le sait pas et nous devons souvent être explicites. Ensuite, le compilateur peut vérifier que la définition de la fonction n'est pas partielle et nous obtenons des garanties de compilation plus fortes.

À travers le point de vue de Curry-Howard, où sont les propositions, alors absurdest une sorte de QED dans une preuve par contradiction.