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

Die absurdFunktion in Data.Voidhat die folgende Signatur, wobei Voidder logisch unbewohnte Typ von diesem Paket exportiert wird:

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

Ich kenne genug Logik, um die Bemerkung der Dokumentation zu erhalten, dass dies durch die Entsprechung von Aussagen als Typen der gültigen Formel entspricht ⊥ → a.

Was mich verwirrt und neugierig macht, ist: Bei welchen praktischen Programmierproblemen ist diese Funktion nützlich? Ich denke, dass es in einigen Fällen vielleicht nützlich ist, um Fälle, die "nicht passieren können", erschöpfend zu behandeln, aber ich weiß nicht genug über die praktische Verwendung von Curry-Howard, um festzustellen, ob diese Idee auf dem Spiel steht überhaupt der richtige Weg.

EDIT: Beispiele vorzugsweise in Haskell, aber wenn jemand eine abhängig getippte Sprache verwenden möchte, werde ich mich nicht beschweren ...

Das Leben ist ein bisschen hart, da Haskell nicht streng ist. Der allgemeine Anwendungsfall besteht darin, unmögliche Pfade zu behandeln. Beispielsweise

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

Dies erweist sich als etwas nützlich. Betrachten Sie einen einfachen Typ fürPipes

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

Dies ist eine streng und vereinfachte Version des Standard-Rohrtyps aus der PipesBibliothek von Gabriel Gonzales . Jetzt können wir eine Pipe codieren, die niemals ergibt (dh einen Verbraucher) als

type Consumer a r = Pipe a Void r

das gibt wirklich nie nach. Dies impliziert, dass die richtige Faltregel für a Consumerist

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

oder alternativ, dass Sie den Ertragsfall im Umgang mit Verbrauchern ignorieren können . Dies ist die allgemeine Version dieses Entwurfsmusters: Verwenden Sie polymorphe Datentypen und Voidbeseitigen Sie bei Bedarf die Möglichkeiten.

Die wahrscheinlich klassischste Verwendung Voidist CPS.

type Continuation a = a -> Void

Das heißt, a Continuationist eine Funktion, die niemals zurückkehrt. Continuationist die Typversion von "nicht". Daraus erhalten wir eine CPS-Monade (entsprechend der klassischen Logik)

newtype CPS a = Continuation (Continuation a)

Da Haskell rein ist, können wir nichts aus diesem Typ herausholen.

Betrachten Sie diese Darstellung für Lambda-Begriffe, die durch ihre freien Variablen parametrisiert sind. (Siehe Artikel 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 einem FunctorBegriff machen , der den Begriff des Umbenennens und Monadden 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 geschlossenen Begriffe: Dies sind die Einwohner von Tm Void. Sie sollten in der Lage sein, die geschlossenen Begriffe in Begriffe mit beliebigen freien Variablen einzubetten. Wie?

fmap absurd :: Tm Void -> Tm a

Der Haken ist natürlich, dass diese Funktion den Begriff durchquert und genau nichts tut. Aber es ist ein Hauch ehrlicher als unsafeCoerce. Und deshalb vacuouswurde hinzugefügt, um Data.Void...

Oder schreiben Sie einen Bewerter. 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, in der freie Variablen aWerten zugeordnet werden 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

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

eval absurd :: Tm Void -> Val b

Im Allgemeinen wird Voides nur 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 die Verwendung einer freien Variablen in einem geschlossenen Begriff). Oft sind diese parametrisierte Typen kommen mit Funktionen höherer Ordnung Operationen an den Parameter - Operationen auf der ganzen Art ( zum Beispiel hier, Heben fmap, >>=, eval). Sie geben also absurdals Allzweckoperation weiter Void.

Stellen Sie sich als weiteres Beispiel vor, Either e vwie Sie Berechnungen erfassen möchten, die Ihnen hoffentlich veine Ausnahme vom Typ geben, aber möglicherweise auslösen e. Sie können diesen Ansatz verwenden, um das Risiko eines schlechten Verhaltens einheitlich zu dokumentieren. Für perfekt verhaltene Berechnungen in dieser Einstellung nehmen Sie ean Voidund verwenden Sie sie

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 einzubetten.

Oh, und ein letztes Hurra, mit einem "kann nicht passieren" umzugehen. Es zeigt sich in der generischen Reißverschlusskonstruktion überall dort, 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 beschlossen, den Rest nicht zu löschen, obwohl er nicht genau 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 sich abenteuerlustig fühlen, zeigt dieser unvollendete Artikel , wie Sie Voiddie Darstellung von Begriffen mit freien Variablen komprimieren können

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

in jeder Syntax, die frei von a Differentiableund Traversablefunctor generiert wird f. Wir verwenden Term f Void, um Regionen ohne freie Variablen [D f (Term f Void)]darzustellen , und um Röhren darzustellen , die durch Regionen ohne freie Variablen entweder zu einer isolierten freien Variablen oder zu einem Knotenpunkt in den Pfaden zu zwei oder mehr freien Variablen tunneln. Muss diesen Artikel irgendwann beenden.

Für einen Typ ohne Werte (oder zumindest keinen, von dem es sich lohnt, in höflicher Gesellschaft zu sprechen) Voidist dies bemerkenswert nützlich. Und absurdso benutzt du es.

Ich denke, dass es in einigen Fällen vielleicht nützlich ist, um Fälle, in denen "nicht passieren kann", erschöpfend zu behandeln

Das ist genau richtig.

Man könnte sagen, das absurdist nicht nützlicher als const (error "Impossible"). Es ist jedoch typbeschränkt, so dass seine einzige Eingabe ein Typ sein kann Void, ein Datentyp, der absichtlich unbewohnt bleibt. Dies bedeutet, dass es keinen tatsächlichen Wert gibt, an den Sie übergeben können absurd. Wenn Sie jemals in einem Codezweig landen, in dem die Typprüfung denkt, dass Sie Zugriff auf etwas Typisches haben Void, befinden Sie sich in einer absurden Situation. Sie absurdmarkieren also grundsätzlich, dass dieser Codezweig niemals erreicht werden sollte.

"Ex falso quodlibet" bedeutet wörtlich "aus [einem] falschen [Satz] folgt alles". Wenn Sie also feststellen, dass Sie ein Datenelement Voidin der Hand haben, dessen Typ es ist , wissen Sie, dass Sie falsche Beweise in Ihren Händen haben. Sie können also jedes gewünschte Loch (via absurd) füllen , da aus einem falschen Satz alles folgt.

Ich habe einen Blog-Beitrag über die Ideen hinter Conduit geschrieben, der ein Beispiel für die Verwendung enthält absurd.

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 teilweise Musterübereinstimmungen zu vermeiden. Beispiel: Eine Annäherung der Datentypdeklarationen aus dieser Antwort :

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 absurdzum Beispiel so verwenden:

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

Es gibt verschiedene Möglichkeiten, den leeren Datentyp darzustellen . Einer ist ein leerer algebraischer Datentyp. Eine andere Möglichkeit besteht darin, es zu einem Alias ​​für ∀α.α oder zu machen

type Void' = forall a . a

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

In einigen Fällen bevorzugen wir die explizite Variante, normalerweise wenn der leere Datentyp in einem Argument einer Funktion oder in einem komplexeren Datentyp wie in Data.Conduit vorkommt :

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

In einigen 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 Darstellungen konvertieren.

Zum Beispiel callcc :: ((a -> m b) -> m a) -> m averwendet (implizit) forall b. Es könnte auch vom Typ sein ((a -> m Void) -> m a) -> m a, da ein Aufruf des Kontingents nicht tatsächlich zurückkehrt, sondern die Kontrolle auf einen anderen Punkt überträgt. Wenn wir mit Fortsetzungen arbeiten wollten, konnten wir definieren

type Continuation r a = a -> Cont r Void

(Wir könnten verwenden, type Continuation' r a = forall b . a -> Cont r baber das würde Rang 2-Typen erfordern.) Und dann vacuousMkonvertiert dies Cont r Voidin Cont r b.

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

In abhängig typisierten Sprachen wie Idris ist es wahrscheinlich nützlicher als in Haskell. Wenn Sie in einer Gesamtfunktion mit einem Wert übereinstimmen, der tatsächlich nicht in die Funktion verschoben werden kann, erstellen Sie normalerweise einen Wert vom Typ "unbewohnt" und verwenden ihn absurdzum Abschluss der Falldefinition.

Diese Funktion entfernt beispielsweise ein Element aus einer Liste mit der dort vorhandenen Costraint auf 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

Wo der zweite Fall besagt, dass eine leere Liste ein bestimmtes Element enthält, 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, ob die Funktionsdefinition nicht partiell ist, und wir erhalten stärkere Garantien für die Kompilierungszeit.

Aus Curry-Howard-Sicht, wo Aussagen sind, ist dann absurdeine Art QED ein Beweis durch Widerspruch.