Negation in Haskell und Purescript

Haskell fetzt! Allerdings ist Haskell in seiner Nische (rein funktionale ML-Sprachen) längst nicht mehr allein. Die moderneren Abkömmlinge dieser Familie bringen hier und da interessante Verbesserungen mit. Ein schönes Beispiel dafür ist die not Funktion in Purescript.

Werte negieren

In Haskell negiert not den Wert eines boolschen Ausdrucks:

-- Haskell GHCi Session
​
> not True
False
​
> not False
True

In Purescript gilt das gleiche:

-- Purescript PSCi Session
​
> not true
false
​
> not false
true

Das ist nicht weiter kompliziert.

Funktionen negieren

Grundsätzlich müssten sich auf die gleiche Weise auch Funktionen negieren lassen, die nach Bool abbilden. Für eine Funktion f :: a -> Bool wäre not f dann ebenfalls eine Funktion a -> Bool, so dass ( not f ) x …

• zu True auswertet wenn f x zu False auswertet, bzw.
• zu False auswertet wenn f x zu True auswertet.

Haskells not kann das nicht leisten. Um das zu demonstrieren, definieren wir eine even Funktion, die entscheidet, ob eine ganze Zahl gerade ist:

-- Haskell GHCi Session
​
> even n = modBy 2 n == 0

> even 0
True
​
> even 1
False
​
> even 2
True
​
> even 3
False

Anmerkung: Mein Haskell ist nicht ganz idiomatisch. modBy ist selbstdefiniert.

Wir müssten also eine odd Funktion definieren können, die entscheidet, ob eine ganze Zahl ungerade ist, indem wir even mit not negieren. Wenn wir versuchen, das in Haskell umzusetzen, scheitern wir:

-- Haskell GHCi Session
​
> odd = not even
<interactive>: error:
    • Couldn't match expected type ‘Bool’ with actual type ‘a0 -> Bool’
    • ...

In Purescript ist das gar kein Problem. Hier ist die even Funktion in Purescript:

-- Purescript PSCi Session
​
> even n = mod n 2 == 0
​
> even 0
true
​
> even 1
false
​
> even 2
true
​
> even 3
false

Wenn wir even mit not negieren, erhalten wir ohne Probleme unsere odd Funktion:

-- Purescript GHCi Session
​
> odd = not even
​
> odd 0
false
​
> odd 1
true
​
> odd 2
false
​
> odd 3
true

Wie ist das umgesetzt?

In Haskell ist not eine Funktion Bool -> Bool. In Purescript ist not eine Funktion HeytingAlgebra a => a -> a. Die Heyting-Algebra ist offenbar eine Verallgemeinerung der booleschen Algebra. Auf den ersten Blick spricht nichts dagegen, not auf die gleiche Weise auch in Haskell zu verallgemeinern. Vielleicht nehme ich das mal in Angriff und versuche not in meinem DIY Prelude entsprechend anzupassen.

Bonus

Dann ist mir noch ein schönes Beispiel dafür eingefallen, dass man manchmal in der Lage ist, zu erkennen, zu welchem Wert ein Ausdruck auswerten müsste, obwohl der Compiler auf dem Schlauch steht:

foldr (+) 0 ( repeat 0 )

Der Ausdruck terminiert weder in Haskell noch in Purescript, weil repeat eine unendliche Sequenz erzeugt. Anschaulich ist völlig klar, dass er zu 0 auswerten müsste, denn wir summieren einfach nur Nullen auf. Formal lässt sich das auch leicht rechtfertigen: wenn wir eine unendliche Summe über einem Monoid bilden, wobei alle Summanden das neutrale Element sind, dann ergibt die Summe schon per Definition ebenfalls das neutrale Element.

Es gibt weitere Beispiele dieser Art. Der folgende Ausdruck terminiert auch nicht, müsste aber zum leeren String "" auswerten. Anschaulich ist das auch wieder völlig klar. Formal gilt das gleiche wie oben.

foldr (++) "" ( repeat "" )

Hinweis: (++) ist hier ein Alias für (<>).

Der folgende Ausdruck terminiert auch nicht, müsste aber in Haskell zur leeren Liste [] auswerten.

foldr (++) [] ( repeat [] )

Spannend ist die Frage, wie man das umsetzen könnte. Alle Beispiele haben die Form:

foldr mappend mempty ( repeat mempty )

Wenn die Faltung in der Lage wäre, diese Form zu erkennen, könnte sie in diesem Fall zu mempty auswerten.