Является ли ложка опасной в Хаскелле?

Итак, библиотека в 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, написанным напрямую.