Чем полезна абсурдная функция в Data.Void?

absurdФункция Data.Voidимеет следующую подпись, где Voidявляется логически необитаемым типом экспортируемого этого пакетом:

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

Я знаю достаточно логики, чтобы получить из документации замечание о том, что это соответствует действительной формуле посредством соответствия предложений как типов ⊥ → a.

Что меня озадачивает и интересует: в каких практических задачах программирования полезна эта функция? Я думаю, что, возможно, в некоторых случаях это полезно как типобезопасный способ исчерпывающей обработки случаев, когда «не может произойти», но я недостаточно знаю о практическом использовании Карри-Ховарда, чтобы сказать, есть ли эта идея на правильный трек вообще.

РЕДАКТИРОВАТЬ: Примеры желательно на Haskell, но если кто-то хочет использовать язык с зависимой типизацией, я не собираюсь жаловаться ...

Жизнь немного трудна, поскольку Haskell не строг. Общий вариант использования - обработка невозможных путей. Например

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

Это оказывается несколько полезным. Рассмотрим простой тип дляPipes

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

это строгая и упрощенная версия стандартного типа pipe из Pipesбиблиотеки Габриэля Гонсалеса . Теперь мы можем закодировать канал, который никогда не уступает (т. Е. Потребитель), как

type Consumer a r = Pipe a Void r

это действительно никогда не поддается. Из этого следует, что правильным правилом складывания для a Consumerявляется

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

или, в качестве альтернативы, вы можете игнорировать вариант yield при работе с потребителями. Это общая версия этого шаблона проектирования: используйте полиморфные типы данных и Voidизбавьтесь от возможностей, когда вам это нужно.

Вероятно, наиболее классическое использование Void- в CPS.

type Continuation a = a -> Void

то есть Continuationфункция, которая никогда не возвращается. Continuationэто типовая версия «не». Отсюда получаем монаду CPS (соответствующую классической логике)

newtype CPS a = Continuation (Continuation a)

поскольку Haskell чист, мы ничего не можем получить от этого типа.

Рассмотрим это представление для лямбда-членов, параметризованных их свободными переменными. (См. Статьи Беллегарда и Хука, 1994 г., Берд и Патерсон, 1999 г., Альтенкирх и Ройс, 1999 г.)

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

Вы, безусловно, можете сделать это a Functor, улавливая понятие переименования и Monadулавливая понятие подстановки.

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

Теперь рассмотрим закрытые условия: это жители Tm Void. Вы должны уметь вставлять закрытые термины в термины с произвольными свободными переменными. Как?

fmap absurd :: Tm Void -> Tm a

Уловка, конечно же, в том, что эта функция будет проходить через термин, ничего не делая. Но это чуть более честно unsafeCoerce. И поэтому vacuousбыл добавлен в Data.Void...

Или напишите оценщику. Вот значения со свободными переменными в b.

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

Я только что представил лямбды как замыкания. Оценщик параметризуется средой, отображающей свободные переменные в aзначениях сверх 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

Ты угадал. Оценить закрытый срок по любой цели

eval absurd :: Tm Void -> Val b

В более общем смысле, Voidредко используется сам по себе, но он удобен, когда вы хотите создать экземпляр параметра типа способом, который указывает на какую-то невозможность (например, здесь, используя свободную переменную в закрытом члене). Часто эти параметризованные типы поставляются с функциями высшего порядка подъемных операций по параметрам операций по всему типу (например, здесь, fmap, >>=, eval). Так что вы проходите absurdкак универсальную операцию по бэкапу Void.

В качестве другого примера представьте, что вы используете Either e vдля захвата вычислений, которые, надеюсь, дадут вам, vно могут вызвать исключение типа e. Вы можете использовать этот подход для единообразного документирования риска плохого поведения. Для прекрасно себя вычисления в этой обстановке, принять , eчтобы быть Void, а затем использовать

either absurd id :: Either Void v -> v

безопасно бежать или

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

внедрять безопасные компоненты в небезопасный мир.

О, и последнее ура, обработка «не может случиться». Он проявляется в общей конструкции застежки-молнии везде, где не может быть курсор.

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!

Остальное решил не удалять, хоть это и не совсем актуально.

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)

Собственно, может быть, это актуально. Если вы любите приключения, в этой незаконченной статье показано, как использовать Voidдля сжатия представления терминов с помощью свободных переменных.

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

в любом синтаксисе свободно генерируется из Differentiableи Traversableфунктора f. Мы используем Term f Voidдля представления областей без свободных переменных и [D f (Term f Void)]для представления трубок, туннелирующих через области без свободных переменных либо к изолированной свободной переменной, либо к стыку на путях к двум или более свободным переменным. Надо когда-нибудь закончить эту статью.

Для типа без значений (или, по крайней мере, такого, о котором стоит говорить в вежливой компании), Voidэто замечательно полезно. И absurdкак вы это используете.

Я думаю, что, возможно, это полезно в некоторых случаях как типобезопасный способ исчерпывающей обработки случаев, когда "не может произойти".

Это совершенно верно.

Можно сказать, что absurdэто не более полезно, чем const (error "Impossible"). Однако он ограничен типом, так что его единственный вход может быть чем-то вроде типа Void, типом данных, который намеренно оставлен необитаемым. Это означает, что нет фактического значения, к которому вы можете перейти absurd. Если вы когда-нибудь попадете в ветвь кода, где средство проверки типов думает, что у вас есть доступ к чему-то типу Void, то, что ж, вы попали в абсурдную ситуацию. Таким образом, вы просто используете, absurdчтобы в основном отметить, что эта ветвь кода никогда не должна быть достигнута.

«Ex falso quodlibet» буквально означает «из ложного [предложения] следует все, что угодно». Поэтому, когда вы обнаруживаете, что Voidхраните данные, тип которых является , вы знаете, что у вас на руках ложные доказательства. Таким образом, вы можете заполнить любую дыру, какую захотите (через absurd), потому что из ложного предложения следует все, что угодно.

Я написал сообщение в блоге об идеях, лежащих в основе Conduit, в котором есть пример использования absurd.

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

Как правило, вы можете использовать его, чтобы избежать частичных совпадений с образцом. Например, получение приблизительного объявления типов данных из этого ответа :

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

Тогда вы могли бы использовать absurd, например, вот так:

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

Есть разные способы представления пустого типа данных . Один из них - это пустой алгебраический тип данных. Другой способ - сделать его псевдонимом для ∀α.α или

type Void' = forall a . a

в Haskell - вот как мы можем закодировать его в Системе F (см. главу 11 Доказательств и типов ). Эти два описания, конечно , изоморфны и изоморфизм засвидетельствовано \x -> x :: (forall a.a) -> Voidи absurd :: Void -> a.

В некоторых случаях мы предпочитаем явный вариант, обычно если пустой тип данных появляется в аргументе функции или в более сложном типе данных, например в Data.Conduit :

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

В некоторых случаях мы предпочитаем полиморфный вариант, обычно пустой тип данных участвует в возвращаемом типе функции.

absurd возникает, когда мы конвертируем эти два представления.

Например, callcc :: ((a -> m b) -> m a) -> m aиспользует (неявно) forall b. Это также может быть тип ((a -> m Void) -> m a) -> m a, потому что вызов продолжения на самом деле не возвращает, он передает управление другой точке. Если бы мы хотели работать с продолжениями, мы могли бы определить

type Continuation r a = a -> Cont r Void

(Мы могли бы использовать, type Continuation' r a = forall b . a -> Cont r bно для этого потребовались бы типы ранга 2.) А затем vacuousMконвертирует это Cont r Voidв Cont r b.

(Также обратите внимание, что вы можете использовать haskellers.com для поиска использования (обратных зависимостей) определенного пакета, например, чтобы узнать, кто и как использует пакет void .)

В языках с зависимой типизацией, таких как Idris, это, вероятно, более полезно, чем в Haskell. Как правило, в итоговой функции при сопоставлении с шаблоном значения, которое на самом деле нельзя вставить в функцию, вы затем создаете значение необитаемого типа и используете его absurdдля завершения определения case.

Например, эта функция удаляет элемент из списка с ограничением уровня типа, которое он там присутствует:

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

Во втором случае говорится, что в пустом списке есть определенный элемент, что является абсурдом. Однако в целом компилятор этого не знает, и нам часто приходится указывать это явно. Затем компилятор может проверить, что определение функции не является частичным, и мы получим более надежные гарантии времени компиляции.

С точки зрения Карри-Ховарда, где утверждения, absurdэто своего рода КЭД в доказательстве от противного.