Ist der Löffel in Haskell unsicher?

Question

So gibt es eine Bibliothek in Haskell spoon genannt, die mir dieses

safeHead :: [a] -> Maybe a 
safeHead = spoon . head 

können tun, aber es lässt mich dieses

>>> 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...> 

auch tun, die in bestimmten Fällen sehr nützlich scheint, aber es verstößt auch gegen denotational Semantik (zu meinem Verständnis), da es mir erlaubt, zwischen verschiedenen Dingen im semantischen Urbild von ⊥ zu unterscheiden. Dies ist strikt leistungsfähiger als throw/catch, da sie wahrscheinlich eine durch Fortsetzungen definierte Semantik haben.

Also meine Frage ist: Kann jemand Löffel böswillig verwenden, um Typ Sicherheit zu brechen? Ist die Bequemlichkeit die Gefahr wert? Oder, realistischer gesehen, gibt es einen vernünftigen Weg, mit dessen Hilfe jemand das Vertrauen in die Bedeutung eines Programms verlieren könnte?

Answer 1

Es gibt einen kniffligen Punkt, an dem, wenn Sie es verwenden, etwas zu tun, was wie ein unschuldiger Refactor scheint, kann das Verhalten eines Programms ändern. Ohne Schnickschnack, ist es das:

f h x = h x 
isJust (spoon (f undefined)) --> True 

aber vielleicht die häufigste Haskell Transformation in dem Buch zu tun, eta Kontraktion, zu f, gibt

f h = h 
isJust (spoon (f undefined)) --> False 

Eta Kontraktion ist bereits nicht Semantik Konservieren wegen der Existenz von seq; aber ohne löffel eta contraction kann nur ein terminierendes programm in einen fehler umwandeln; mit löffel eta contraction kann ein terminierendes programm in ein anderes terminierendes programm ändern.

Formal ist der Weg spoon unsicher ist, dass es non-monotone on domains ist (und somit können so Funktionen definiert werden, in Bezug darauf); wohingegen ohne spoon jede Funktion monoton ist. So technisch verlieren Sie diese nützliche Eigenschaft der formalen Argumentation.

mit einem realen Beispiel kommen, wenn dies wichtig wäre, ist für den Leser als Übung (sprich: Ich denke, dass es sehr unwahrscheinlich ist, im wirklichen Leben Materie - es sei denn, Sie es starten zu missbrauchen; zB mit undefined wie Java Programmierer null verwenden)

Answer 2

Sie können nicht schreiben unsafeCoerce mit spoon, wenn das ist, was Sie bekommen. Es ist genau so unsicher, wie es aussieht, und verletzt die Haskell-Semantik genau so, wie es scheint. Sie können es jedoch nicht verwenden, um einen Segfault oder ähnliches zu erstellen.

Durch Verletzung der Haskell-Semantik macht es jedoch macht machen Code schwieriger, über im Allgemeinen, und auch, z. Ein safeHead mit Löffel wird zwangsläufig weniger effizient als ein safeHead direkt geschrieben werden.