Является ли ложка опасной в Хаскелле?
Итак, библиотека в Haskell называется spoon, которая позволяет мне делать это
safeHead :: [a] -> Maybe a
safeHead = spoon . head
но это также позволяет мне сделать это
>>> spoon True :: Maybe Bool
Just True
>>> spoon (error "fork") :: Maybe Bool
Nothing
>>> spoon undefined :: Maybe Bool
Nothing
>>> spoon (let x = x in x) :: Maybe Bool
<... let just keep waiting...>
который кажется действительно полезным в некоторых случаях, но он также нарушает денотационную семантику (на мой взгляд), поскольку он позволяет мне различать разные вещи в семантическом прообразе ⊥. Это строго более мощное, чем throw/catch, поскольку они, вероятно, имеют семантику, определенную продолжениями.
>>> try $ return (error "thimble") :: IO (Either SomeException Bool)
Right *** Exception: thimble
Итак, мой вопрос: может ли кто-то использовать ложку злонамеренно, чтобы нарушить безопасность типа? Это удобство стоит опасности? Или, что более реалистично, существует ли разумный способ, что использование этого может подорвать доверие к значению программы?
Ответы
Ответ 1
Есть одна сложная точка, где, если вы ее используете, то, что кажется невиновным рефактором, может изменить поведение программы. Без каких-либо звонков и свистков он:
f h x = h x
isJust (spoon (f undefined)) --> True
но, возможно, наиболее распространенное преобразование haskell в книге, eta сокращение, до f, дает
f h = h
isJust (spoon (f undefined)) --> False
Это сжатие уже не является семантикой, сохраняющейся из-за существования seq; но без spoon eta сокращение может только изменить программу завершения в ошибку; с сокращением spoon eta может изменить завершающую программу в другую завершающую программу.
Формально, путь spoon небезопасен, так это немонотонно на доменах (и, следовательно, поэтому могут быть функции, определенные в терминах его); тогда как без spoon каждая функция монотонна. Так технически вы теряете это полезное свойство формальных рассуждений.
Придумывая реальный пример того, когда это будет важно, остается как упражнение для читателя (читайте: я думаю, что это вряд ли имеет значение в реальной жизни - если вы не начнете его злоупотреблять, например, используя undefined способ использования Java-программистов null)
Ответ 2
Вы не можете написать unsafeCoerce с помощью spoon, если это то, что вы получаете. Это так же плохо, как кажется, и нарушает семантику Хаскелла точно так же, как кажется. Однако вы не можете использовать его для создания segfault или чего-либо подобного.
Однако, нарушая семантику Haskell, это делает код сложнее рассуждать вообще, а также, например, a safeHead с ложкой обязательно будет менее эффективным, чем a safeHead, написанным напрямую.
