Kirche Codierung von boolean und STLC

Question

Es wird oft gesagt, dass

tru t f = t 
fls t f = f 

Wahr und Falsch in dem Sinne darstellen, dass „wir diese Begriffe verwenden können, um die Prüfung der Wahrheit eines Booleschen Wert, den Vorgang auszuführen“.

Aber das verbirgt eine wichtige Einschränkung darin, dass es nur in der untypisierten Lambda-Kalkül wahr scheint. Wenn ich diese Werte in Haskell einfach anschließen, kann ich eine Funktion schreiben:

tryMeOnFalse ∷ (∀ t f. t → f → t) → String 
tryMeOnFalse tr = "Hi" 
a' = tryMeOnFalse tru 
b' = tryMeOnFalse fls -- type error ! 

die tru und fls auf der Typebene unterscheidet. Wie falsch/wahr wäre es, das zu sagen:

• in STLC tru und fls Wert Ebene Zeuge einiger gefördert 'Boolean Art sind, die Typen 'True und 'False
• in STLC der (erzwungenen) eingegeben Werte hat und (fls :: ∀ t . t → t → t) repräsentieren Wahr und Falsch (und in nicht typisiert, auch die übliche)

Edit: ich weiß jetzt, dank @ Daniel Wagner Antwort ich dachte an zweiter Ordnung Lambda-Kalkül und nicht sTLC in meinem questi auf.

Answer 1

Dies gilt nicht nur für den untypisierten Lambda-Kalkül; aber in typisierten Kalkülen muss man wie üblich vorsichtig mit dem Tippen umgehen. Wir definieren sollten:

type Boolean = forall r. r -> r -> r 

wir sicherlich tru, fls :: Boolean haben, und sollten auch als solche mit Anmerkungen versehen. Aber wir tun nicht haben tryMeOnFalse :: Boolean -> String! Es gibt also keinen wirklichen Widerspruch.

Ihre Kommentare zu STLC sind etwas komisch, da STLC ein ganz anderes Schreibsystem hat. Wir würden für jeden Ergebnistyp dort getrennte boolesche Typen benötigen, da kein Polymorphismus ist.

In Haskell, kann man mit Sicherheit Typen definieren, die von tru nur besiedelt sind oder nur durch fls (gut, ist jeder Typ auch durch undefined bewohnt, natürlich); aber das ist im Allgemeinen nicht sehr nützlich.