Wofür ist die absurde Funktion in Data.Void nützlich?

Betrachten Sie diese Darstellung für Lambda-Terme, die durch ihre freien Variablen parametrisiert werden. (Siehe Papiere von Bellegarde und Hook 1994, Bird und Paterson 1999, Altenkirch und Reus 1999.)

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

Sie können dies sicherlich zu einer Functor machen, die den Begriff der Umbenennung erfasst, und eine Monad, die den Begriff der Substitution erfasst.

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

Betrachten Sie nun die closed -Begriffe: Dies sind die Einwohner von Tm Void. Sie sollten in der Lage sein, die geschlossenen Terme mit beliebigen freien Variablen in Terme einzubetten. Wie?

fmap absurd :: Tm Void -> Tm a

Der Haken ist natürlich, dass diese Funktion den Begriff überschreitet, indem er genau nichts tut. Aber es ist eine ehrlichere Note als unsafeCoerce. Und deshalb wurde vacuous zu Data.Void... hinzugefügt.

Oder schreibe einen Evaluator. Hier sind Werte mit freien Variablen in b.

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

Ich habe gerade Lambdas als Verschlüsse dargestellt. Der Evaluator wird durch eine Umgebung parametrisiert, die freie Variablen in a mit Werten über b abbildet.

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

Du hast es erraten. Um einen geschlossenen Begriff an einem beliebigen Ziel zu bewerten

eval absurd :: Tm Void -> Val b

Allgemein wird Void selten alleine verwendet, ist jedoch praktisch, wenn Sie einen Typparameter auf eine Weise instanziieren möchten, die auf eine Art Unmöglichkeit hinweist (z. B. hier, wenn Sie eine freie Variable in einem geschlossenen Begriff verwenden). Häufig sind diese parametrisierten Typen mit Funktionen höherer Ordnung ausgestattet, die Operationen an den Parametern des gesamten Typs anheben (z. B. hier fmap, >>=, eval). Sie übergeben also absurd als Allzweckoperation für Void.

Stellen Sie sich für ein anderes Beispiel vor, Sie verwenden Either e v zum Erfassen von Berechnungen, die Ihnen hoffentlich eine v geben, die jedoch eine Ausnahme vom Typ e auslösen kann. Sie können diesen Ansatz verwenden, um das Risiko eines Fehlverhaltens einheitlich zu dokumentieren. Für einwandfrei verhaltene Berechnungen in dieser Einstellung nehmen Sie e als Void an und verwenden Sie dann

either absurd id :: Either Void v -> v

sicher laufen oder

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

sichere Komponenten in eine unsichere Welt einbetten.

Oh, und noch ein letztes Hurra, ein "kann nicht passieren". Es zeigt sich in der generischen Reißverschlusskonstruktion überall, wo der Cursor nicht sein kann.

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!

Ich habe mich entschieden, den Rest nicht zu löschen, auch wenn es nicht gerade relevant ist.

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)

Eigentlich ist es vielleicht relevant. Wenn Sie abenteuerlustig sind, zeigt dieser unfertige Artikel , wie Sie mit Void die Darstellung von Begriffen mit freien Variablen komprimieren

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

in einer beliebigen Syntax, die frei aus einem Differentiable- und Traversable-Funktor f generiert wurde. Wir verwenden Term f Void, um Regionen ohne freie Variablen darzustellen, und [D f (Term f Void)], um tubes darzustellen, die durch Regionen ohne freie Variablen zu einer isolierten freien Variablen oder zu einer Kreuzung in den Pfaden zu zwei oder mehr freien Variablen tunneln. Muss diesen Artikel irgendwann beenden.

Für einen Typ ohne Werte (oder zumindest keinen Wert, der in höflicher Gesellschaft anspricht) ist Void bemerkenswert nützlich. Und absurd benutzt du so.

Ich denke, dass es in manchen Fällen nützlich sein kann, wenn es darum geht, "Fälle", die nicht passieren können, erschöpfend zu behandeln

Das ist genau richtig.

Man könnte sagen, dass absurd nicht nützlicher ist als const (error "Impossible"). Es ist jedoch auf den Typ beschränkt, so dass seine einzige Eingabe etwas vom Typ Void sein kann, ein Datentyp, der absichtlich unbewohnt bleibt. Das heißt, es gibt keinen tatsächlichen Wert, den Sie an absurd übergeben können. Wenn Sie in einem Codezweig landen, in dem der Typprüfer den Eindruck hat, dass Sie Zugriff auf etwas vom Typ Void haben, befinden Sie sich in einer Situation absurd. Sie verwenden also absurd, um im Grunde zu markieren, dass dieser Zweig des Codes niemals erreicht werden sollte.

"Ex falso quodlibet" bedeutet wörtlich "aus [einem falschen] Satz, alles folgt". Wenn Sie also feststellen, dass Sie ein Datenelement halten, dessen Typ Void ist, wissen Sie, dass Sie falsche Beweise in Ihrer Hand haben. Sie können also any _ hole (über absurd) füllen, da aus einem falschen Satz alles folgt.

Ich habe einen Blogbeitrag über die Ideen hinter Conduit geschrieben, die ein Beispiel für die Verwendung von absurd enthalten. 

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

Im Allgemeinen können Sie es verwenden, um scheinbar partielle Musterübereinstimmungen zu vermeiden. Wenn Sie beispielsweise eine Annäherung an die Datentypdeklarationen aus dieser Antwort ziehen:

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

Dann könnten Sie absurd wie folgt verwenden:

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

Es gibt verschiedene Arten, wie der leere Datentyp dargestellt werden soll. Einer ist ein leerer algebraischer Datentyp. Eine andere Möglichkeit ist, es als Alias ​​für ∀α.α oder zu verwenden

type Void' = forall a . a

in Haskell - so können wir es in System F kodieren (siehe Kapitel 11 von Proofs and Types ). Diese beiden Beschreibungen sind natürlich isomorph und der Isomorphismus wird von \x -> x :: (forall a.a) -> Void und von absurd :: Void -> a beobachtet.

In manchen Fällen bevorzugen wir die explizite Variante, in der Regel, wenn der leere Datentyp in einem Argument einer Funktion oder in einem komplexeren Datentyp angezeigt wird, beispielsweise in Data.Conduit :

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

In manchen Fällen bevorzugen wir die polymorphe Variante, normalerweise ist der leere Datentyp am Rückgabetyp einer Funktion beteiligt.

absurd entsteht, wenn wir zwischen diesen beiden Repräsentationen konvertieren.

Beispielsweise verwendet callcc :: ((a -> m b) -> m a) -> m a (implizit) forall b. Es könnte auch vom Typ ((a -> m Void) -> m a) -> m a sein, da ein Aufruf zur Kontinierung nicht wirklich zurückkehrt, sondern die Kontrolle an einen anderen Punkt überträgt. Wenn wir mit Fortsetzungen arbeiten wollten, könnten wir definieren

type Continuation r a = a -> Cont r Void

(Wir könnten type Continuation' r a = forall b . a -> Cont r b verwenden, aber das würde Rang 2-Typen erfordern.) Und dann vacuousM konvertiert diesen Cont r Void in Cont r b.

(Beachten Sie auch, dass Sie haskellers.com verwenden können, um nach Verwendung (umgekehrte Abhängigkeiten) eines bestimmten Pakets zu suchen, z. B. um zu sehen, wer und wie das Paket void verwendet wird.)

In abhängig typisierten Sprachen wie Idris ist es wahrscheinlich nützlicher als in Haskell. Normalerweise würden Sie in einer Total-Funktion, wenn Sie mit einem Muster einen Wert angeben, der eigentlich nicht in die Funktion eingefügt werden kann, einen unbewohnten Wert erstellen und die Variablendefinition mit absurd abschließen. 

Diese Funktion entfernt beispielsweise ein Element aus einer Liste mit der dort vorhandenen Typebene.

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

Wenn der zweite Fall besagt, dass sich in einer leeren Liste ein bestimmtes Element befindet, was durchaus absurd ist. Im Allgemeinen weiß der Compiler dies jedoch nicht und wir müssen oft explizit sein. Dann kann der Compiler überprüfen, dass die Funktionsdefinition nicht unvollständig ist, und wir erhalten stärkere Kompilierzeitgarantien.

Durch den Standpunkt von Curry-Howard, wo Vorschläge sind, ist absurd eine Art QED in einem widersprüchlichen Beweis.