Для чего нужна абсурдная функция в 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,
Я озадачен и удивлен: в каких практических задачах программирования эта функция полезна? Я думаю, что, возможно, в некоторых случаях он полезен как безопасный для типов способ исчерпывающей обработки случаев "не может произойти", но я не знаю достаточно о практическом использовании Curry-Howard, чтобы определить, присутствует ли эта идея в правильный путь на всех.
РЕДАКТИРОВАТЬ: Примеры желательно в Haskell, но если кто-то хочет использовать зависимый типизированный язык, я не собираюсь жаловаться...
6 ответов
Жизнь немного сложна, поскольку Хаскелл не строг. Общий вариант использования - обработка невозможных путей. Например
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)
это упрощенная и упрощенная версия стандартного типа труб от Габриэля Гонзалеса. Pipes библиотека. Теперь мы можем закодировать канал, который никогда не выдаст (т. Е. Потребителя) как
type Consumer a r = Pipe a Void r
это действительно никогда не дает. Следствием этого является то, что правильное правило сгиба для 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
это Continuation это функция, которая никогда не возвращается. Continuation это версия типа "нет". Отсюда получаем монаду CPS (соответствующую классической логике)
newtype CPS a = Continuation (Continuation a)
поскольку Хаскелл чист, мы не можем ничего получить из этого типа.
Рассмотрим это представление для лямбда-членов, параметризованных их свободными переменными. (См. Документы Bellegarde and Hook 1994, Bird and Paterson 1999, Altenkirch and 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 как ты это используешь.
Я думаю, что, возможно, это полезно в некоторых случаях как безопасный для типов способ исчерпывающей обработки случаев "не может быть"
Это точно верно.
Ты мог сказать это 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/
Существуют разные способы представления пустого типа данных. Одним из них является пустой алгебраический тип данных. Другой способ - создать псевдоним для ∀α.α или
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.)
Как правило, вы можете использовать его, чтобы избежать частичного совпадения с образцом. Например, получение аппроксимации объявлений типов данных из этого ответа:
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
В языках с зависимой типизацией, таких как Idris, это, вероятно, более полезно, чем в 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 является своего рода КЭД в доказательстве от противного.