Рассмотрите это представление для лямбда-терминов, параметризованных их свободными переменными. (См документы от Bellegarde и Hook 1994, Птица и Патерсон 1999, Altenkirch и Реус 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)
На самом деле, может быть, это актуально. Если вы чувствуете приключений, это unfinished article показывает, как использовать 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', посвященная монаде' Cont': http://www.haskellforall.com/2012/12/the-continuation-monad.html – Artyom
Вы может видеть «абсурдным» как одно из направлений изоморфизма между «Пустотой» и «forall a». a'. –