Do czego przydatna jest absurdalna funkcja w Data.Void?

absurdFunkcja w Data.Voidma następujący podpis, gdzie Voidjest logicznie niezamieszkana typ eksportowane przez ten pakiet:

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

Znam wystarczająco logikę, aby uzyskać uwagę dokumentacji, że odpowiada to, poprzez zgodność twierdzeń jako typów, prawidłowej formule ⊥ → a.

Jestem zdziwiony i ciekawy: w jakich praktycznych problemach programistycznych ta funkcja jest przydatna? Myślę, że być może jest to przydatne w niektórych przypadkach jako bezpieczny dla typu sposób wyczerpującej obsługi przypadków „nie może się zdarzyć”, ale nie wiem wystarczająco dużo o praktycznych zastosowaniach Curry-Howarda, aby stwierdzić, czy ten pomysł jest w w ogóle właściwy tor.

EDYCJA: Przykłady najlepiej w Haskell, ale jeśli ktoś chce używać zależnie pisanego języka, nie będę narzekać ...

Życie jest trochę trudne, ponieważ Haskell nie jest surowy. Ogólnym przypadkiem użycia jest obsługa niemożliwych ścieżek. Na przykład

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

Okazuje się, że jest to dość przydatne. Rozważ prosty typ dlaPipes

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

jest to ścisła i uproszczona wersja standardowego typu potoków z Pipesbiblioteki Gabriela Gonzalesa . Teraz możemy zakodować potok, który nigdy nie daje (tj. Konsument) jako

type Consumer a r = Pipe a Void r

to naprawdę nigdy nie ustąpi. Wynika z tego, że prawidłowa reguła fold dla a Consumerjest

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

lub alternatywnie, że możesz zignorować przypadek rentowności w kontaktach z konsumentami. To jest ogólna wersja tego wzorca projektowego: użyj polimorficznych typów danych i Voidpozbądź się możliwości, gdy zajdzie taka potrzeba.

Prawdopodobnie najbardziej klasycznym zastosowaniem Voidjest CPS.

type Continuation a = a -> Void

to znaczy a Continuationjest funkcją, która nigdy nie zwraca. Continuationjest wersją typu „not”. Z tego otrzymujemy monadę CPS (odpowiadającą logice klasycznej)

newtype CPS a = Continuation (Continuation a)

ponieważ Haskell jest czysty, nie możemy nic z tego wyciągnąć.

Rozważ tę reprezentację dla wyrażeń lambda sparametryzowanych przez ich wolne zmienne. (Patrz artykuły Bellegarde i Hook 1994, Bird i Paterson 1999, Altenkirch i Reus 1999.)

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

Z pewnością możesz to uczynić Functor, przechwytując pojęcie zmiany nazwy i Monadprzechwytując pojęcie zastępowania.

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

Rozważmy teraz zamknięte warunki: to są mieszkańcy Tm Void. Powinieneś być w stanie osadzić zamknięte warunki w terminach z dowolnymi wolnymi zmiennymi. W jaki sposób?

fmap absurd :: Tm Void -> Tm a

Haczyk polega oczywiście na tym, że ta funkcja przejdzie przez termin dokładnie nic nie robiąc. Ale to odrobinę bardziej szczere niż unsafeCoerce. I dlatego vacuouszostał dodany do Data.Void...

Lub napisz ewaluatora. Oto wartości z wolnymi zmiennymi w b.

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

Przedstawiłem właśnie lambdy jako zamknięcia. Ewaluator jest parametryzowany przez środowisko odwzorowujące wolne zmienne ana wartości powyżej 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

Zgadłeś. Aby ocenić zamknięty termin w dowolnym celu

eval absurd :: Tm Void -> Val b

Mówiąc bardziej ogólnie, Voidjest rzadko używany samodzielnie, ale jest przydatny, gdy chcesz utworzyć wystąpienie parametru typu w sposób wskazujący na jakąś niemożliwość (np. Tutaj, używając wolnej zmiennej w zamkniętym terminie). Często te parametryzowane typy pochodzą z funkcji wyższego rzędu operacji podnoszenia od parametrów operacji na całym typu (na przykład tutaj fmap, >>=, eval). Więc przekazujesz absurdjako operację ogólnego przeznaczenia Void.

Na przykład, wyobraź sobie użycie Either e vdo przechwytywania obliczeń, które, miejmy nadzieję, dają ci, vale mogą wywołać wyjątek typu e. Możesz użyć tego podejścia do jednolitego dokumentowania ryzyka złego zachowania. Aby uzyskać doskonale wykonane obliczenia w tym ustawieniu, weź eje Void, a następnie użyj

either absurd id :: Either Void v -> v

bezpiecznie biegać lub

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

aby osadzić bezpieczne komponenty w niebezpiecznym świecie.

Aha, i ostatni hurra, radzenie sobie z „nie może się zdarzyć”. Pojawia się w ogólnej konstrukcji zamka błyskawicznego, wszędzie tam, gdzie nie może znajdować się kursor.

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!

Postanowiłem nie usuwać reszty, mimo że nie jest to do końca istotne.

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)

Właściwie może to ma znaczenie. Jeśli masz ochotę na przygodę, ten niedokończony artykuł pokazuje, jak Voidskompresować reprezentację terminów za pomocą wolnych zmiennych

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

w dowolnej składni generowanej swobodnie z funktora Differentiablei . Używamy do reprezentowania regionów bez wolnych zmiennych i do przedstawiania tuneli rurowych przez regiony bez wolnych zmiennych albo do izolowanej zmiennej wolnej, albo do skrzyżowania ścieżek do dwóch lub więcej zmiennych wolnych. Muszę kiedyś skończyć ten artykuł.TraversablefTerm f Void[D f (Term f Void)]

Dla typu bez wartości (a przynajmniej takich, o których warto mówić w grzecznym towarzystwie), Voidjest niezwykle przydatne. I absurdjak tego używasz.

Myślę, że być może jest to przydatne w niektórych przypadkach jako bezpieczny dla typu sposób wyczerpującej obsługi przypadków „nie może się zdarzyć”

Dokładnie tak.

Można powiedzieć, że absurdnie jest to bardziej przydatne niż const (error "Impossible"). Jednak jest to typ ograniczony, więc jego jedyne wejście może być czymś typu Void, typem danych, który jest celowo pozostawiony niezamieszkany. Oznacza to, że nie ma rzeczywistej wartości, do której można przejść absurd. Jeśli kiedykolwiek znajdziesz się w gałęzi kodu, w której kontroler typów myśli, że masz dostęp do czegoś w rodzaju Void, to cóż, jesteś w absurdalnej sytuacji. Więc po prostu używasz absurddo zaznaczenia, że ​​ta gałąź kodu nigdy nie powinna zostać osiągnięta.

„Ex falso quodlibet” dosłownie oznacza „z [a] fałszywego [zdania], wszystko następuje”. Kiedy więc stwierdzisz, że trzymasz w ręku dane, których typ jest Void, wiesz, że masz w rękach fałszywe dowody. Możesz zatem wypełnić dowolną lukę (przez absurd), ponieważ z fałszywej propozycji wszystko wynika.

Napisałem post na blogu o ideach Conduit, który ma przykład użycia absurd.

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

Ogólnie można go użyć, aby uniknąć pozornie częściowych dopasowań wzorców. Na przykład, pobierając przybliżenie deklaracji typu danych z tej odpowiedzi :

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

Wtedy możesz użyć w absurdten sposób, na przykład:

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

Istnieją różne sposoby przedstawiania pustego typu danych . Jeden to pusty algebraiczny typ danych. Innym sposobem jest utworzenie aliasu dla ∀α.α lub

type Void' = forall a . a

w Haskell - w ten sposób możemy zakodować to w Systemie F (zobacz Rozdział 11, Dowody i typy ). Te dwa opisy są oczywiście izomorficzne, a izomorfizm jest obserwowany przez \x -> x :: (forall a.a) -> Voidi przez absurd :: Void -> a.

W niektórych przypadkach preferujemy wariant jawny, zwykle jeśli pusty typ danych pojawia się w argumencie funkcji lub w bardziej złożonym typie danych, takim jak Data.Conduit :

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

W niektórych przypadkach preferujemy wariant polimorficzny, zwykle pusty typ danych jest zaangażowany w typ zwracany przez funkcję.

absurd pojawia się, gdy dokonujemy konwersji między tymi dwoma reprezentacjami.

Na przykład callcc :: ((a -> m b) -> m a) -> m auses (implicit) forall b. Może to być również typ ((a -> m Void) -> m a) -> m a, ponieważ wywołanie kontinacji w rzeczywistości nie zwraca, ale przekazuje kontrolę do innego punktu. Gdybyśmy chcieli pracować z kontynuacjami, moglibyśmy zdefiniować

type Continuation r a = a -> Cont r Void

(Moglibyśmy użyć, type Continuation' r a = forall b . a -> Cont r bale wymagałoby to typów rangi 2.) A potem vacuousMkonwertuje to Cont r Voidna Cont r b.

(Pamiętaj również, że możesz użyć witryny haskellers.com, aby wyszukać użycie (odwrotne zależności) określonego pakietu, na przykład sprawdzić, kto i jak używa void pakietu.)

W językach zależnych, takich jak Idris, jest to prawdopodobnie bardziej przydatne niż w Haskell. Zwykle w funkcji total, gdy dopasujesz wzorzec do wartości, której w rzeczywistości nie można wstawić do funkcji, konstruujesz wartość typu niezamieszkanego i używasz absurddo sfinalizowania definicji przypadku.

Na przykład ta funkcja usuwa element z listy z ograniczeniem kosztu na poziomie typu, który jest tam obecny:

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

Gdzie drugi przypadek mówi, że na pustej liście jest pewien element, co jest całkiem absurdalne. Generalnie jednak kompilator tego nie wie i często musimy to wyraźnie określić. Wtedy kompilator może sprawdzić, czy definicja funkcji nie jest częściowa i uzyskujemy silniejsze gwarancje czasu kompilacji.

Z punktu widzenia Curry-Howarda, gdzie są twierdzenia, absurdjest to rodzaj QED w dowodzie przez sprzeczność.