La cuillère est-elle dangereuse en Haskell ?

Question

Il existe donc une bibliothèque en Haskell appelée cuillère ce qui me permet de faire ceci

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

mais il me permet aussi de faire ceci

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

ce qui semble très utile dans certains cas, mais qui viole également la sémantique dénotationnelle (à mon sens) puisqu'elle me permet de distinguer différentes choses dans la pré-image sémantique de . C'est strictement plus puissant que throw / catch puisqu'ils ont probablement une sémantique définie par les continuations.

>>> try $ return (error "thimble") :: IO (Either SomeException Bool)
Right *** Exception: thimble

Ma question est donc la suivante : quelqu'un peut-il utiliser spoon de manière malveillante pour enfreindre la sécurité des caractères ? Le confort d'utilisation vaut-il le danger ? Ou, de manière plus réaliste, existe-t-il un moyen raisonnable d'éroder la confiance de quelqu'un dans la signification d'un programme ?

Answer 1

Il y a un point délicat où, si vous l'utilisez, ce qui semble être un refactoring innocent peut changer le comportement d'un programme. Sans aucun artifice, c'est ceci :

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

mais en effectuant la transformation haskell la plus courante, la contraction de eta, en f , donne

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

La contraction Eta ne préserve déjà pas la sémantique en raison de l'existence de seq ; mais sans la contraction spoon eta, on ne peut que transformer un programme terminant en erreur ; avec la contraction spoon eta, on peut transformer un programme terminant en un programme terminant différent.

Formellement, la façon dont spoon n'est pas sûre, c'est qu'elle est non monotone sur les domaines (et peuvent donc être des fonctions définies en termes de celle-ci) ; alors qu'en l'absence de spoon toute fonction est monotone. Ainsi, les techniquement vous perdez cette propriété utile du raisonnement formel.

L'élaboration d'un exemple concret de cas où cela serait important est laissée à l'appréciation du lecteur (lire ) : Je pense qu'il est très peu probable que cela ait de l'importance dans la vie réelle -- sauf si vous commencez à en abuser, par exemple en utilisant undefined à la manière dont les programmeurs Java utilisent null )

Answer 2

Vous ne pouvez pas écrire unsafeCoerce con spoon si c'est ce à quoi vous voulez en venir. Il est précisément aussi peu solide qu'il en a l'air, et viole la sémantique Haskell précisément autant qu'il en a l'air. Cependant, vous ne pouvez pas l'utiliser pour créer un segfault ou quoi que ce soit de ce genre.

Cependant, en violant la sémantique de Haskell, elle fait rendent le code plus difficile à raisonner en général, et aussi, par exemple, une safeHead avec une cuillère sera nécessairement moins efficace qu'un safeHead écrit directement.