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

Ответ 1

Жизнь немного сложна, так как 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)

это строгая и упрощенная версия стандартного типа труб из библиотеки Gabriel Gonzales 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

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

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

type Continuation a = a -> Void

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

newtype CPS a = Continuation (Continuation a)

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

Ответ 2

Рассмотрим это представление для лямбда-членов, параметризованных их свободными переменными. (См. Работы Bellegarde and Hook 1994, Bird and Paterson 1999, Altenkirch и Reus 1999.)

data Tm a  = Var a
           | Tm a :$ Tm a
           | Lam (Tm (Maybe 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 заключается в том, как вы его используете.

Ответ 3

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

Это правильно.

Можно сказать, что 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

Ответ 4

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

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

Ответ 5

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

type Void' = forall a . a

в Haskell - так мы можем кодировать его в System 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.)

Ответ 6

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

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

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 является своего рода КЭД в доказательстве от противного.