Eglise de codage booléen et STLC

Question

On dit souvent que

tru t f = t 
fls t f = f 

représentent Vrai et faux dans le sens que « nous pouvons utiliser ces termes pour effectuer l'opération sur le test de la vérité d'une valeur booléenne ». Mais cela cache une mise en garde importante en ce sens que cela ne semble vrai que dans le lambda-calcul non typé. Si je viens de brancher ces valeurs dans haskell, je peux écrire une fonction:

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

qui tru distingue et fls au niveau du type. Quelle erreur/vrai serait-il de dire que:

• dans STLC tru et fls sont témoins de niveau de valeur de certains promu 'Boolean genre, qui a des types 'True et 'False
• en STLC le (sous la contrainte) typée valeurs et (fls :: ∀ t . t → t → t) représentent Vrai et Faux (et typées, bien l'habituel)

Edit: Je me rends compte maintenant grâce à la réponse de Wagner @ Daniel Je pensais second ordre Lambda Calcul et non STLC dans mon questi sur.

Answer 1

Ce n'est pas seulement vrai dans le lambda-calcul non typé; mais dans les calculs typés, il faut être un peu prudent avec la frappe, comme d'habitude. Nous devons définir:

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

Nous avons certainement tru, fls :: Boolean, et devrait les annoter en tant que tel. Mais nous faisons pas avons tryMeOnFalse :: Boolean -> String! Il n'y a donc pas de véritable contradiction ici. Vos commentaires à propos de STLC sont un peu bizarres, puisque STLC a un système de typage très différent. Nous aurions besoin de types booléens séparés pour chaque type de résultat, puisqu'il y a aucun polymorphisme.

Dans Haskell, on peut certainement définir des types qui sont habitées que par tru ou seulement par fls (bien, chaque type est également habité par undefined, bien sûr); mais ce n'est généralement pas très utile.