Ложка небезопасна в Хаскеле?
Итак, в Хаскеле есть библиотека, которая называется " Ложка", которая позволяет мне делать это.
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's just keep waiting...>
который в некоторых случаях кажется действительно полезным, но он также нарушает денотационную семантику (на мой взгляд), поскольку позволяет мне различать разные вещи в семантическом прообразе ⊥
, Это строго сильнее, чем throw
/catch
так как они, вероятно, имеют семантику, определяемую продолжениями.
>>> try $ return (error "thimble") :: IO (Either SomeException Bool)
Right *** Exception: thimble
Поэтому мой вопрос: может ли кто-то использовать ложку злонамеренно, чтобы нарушить безопасность типов? Стоит ли удобство опасности? Или, более реалистично, есть ли разумный способ, которым его использование могло бы подорвать чью-то уверенность в значении программы?
2 ответа
Есть один сложный момент, когда, если вы его используете, выполнение того, что кажется невинным рефакторингом, может изменить поведение программы. Без наворотов, вот так:
f h x = h x
isJust (spoon (f undefined)) --> True
но делать, пожалуй, самое распространенное преобразование haskell в книге, это сокращение, чтобы f
дает
f h = h
isJust (spoon (f undefined)) --> False
Это сокращение уже не сохраняет семантику из-за существования seq
; но без ложки это сокращение может только превратить завершающую программу в ошибку; с помощью ложки это сокращение может изменить программу завершения в другую программу завершения.
Формально, кстати spoon
небезопасно то, что он немонотонен в доменах (и, следовательно, так могут быть функции, определенные в терминах этого); тогда как без spoon
каждая функция монотонна. Технически, вы теряете это полезное свойство формальных рассуждений.
Придумать пример из реальной жизни, когда это было бы важно, оставлено в качестве упражнения для читателя (читай: я думаю, что это вряд ли имеет значение в реальной жизни - если вы не начнете злоупотреблять им, например, используя undefined
как Java-программисты используют null
)
Ты не можешь писать unsafeCoerce
с spoon
, если это то, к чему ты клонишь. Это так же несостоятельно, как выглядит, и нарушает семантику Хаскелла точно так же, как кажется. Тем не менее, вы не можете использовать его для создания ошибки или чего-то подобного.
Однако, нарушая семантику Haskell, это делает код труднее рассуждать в целом, а также, например, safeHead
с ложкой обязательно будет менее эффективным, чем safeHead
написано напрямую.