Logique combinatoire simplement saisie?

Comme il existe un calcul lambda non typé et un calcul lambda simplement tapé (comme décrit, par exemple, dans le livre Types et langages de programmation de Benjamin Pierce), existe-t-il une logique combinatoire simplement tapée?

Par exemple, il semblerait que les types naturels des combinateurs S, K et I seraient

S : (a -> b -> c) -> (a -> b) -> a -> c
K : a -> b -> a
I : a -> a

où a, b et c sont des variables de type s'étendant sur un ensemble de types T. Maintenant, nous pourrions peut-être commencer avec un seul type de base, Bool. Notre ensemble de types T est alors Bool avec tous les types qui peuvent être formés en utilisant les trois modèles

(a -> b -> c) -> (a -> b) -> a -> c
a -> b -> a
a -> a

où a, b, c dans T.

Il y aurait deux nouvelles constantes dans le langage.

T : Bool
F : Bool

Ainsi, ce langage se compose des symboles S, K, I, T et F, ainsi que des parenthèses. Il a un type de base Bool et les "types de fonctions" qui peuvent être créés à partir des modèles de combinateur S, K et I.

Ce système peut-il fonctionner? Par exemple, existe-t-il une construction bien typée si-alors-autre qui peut être formée uniquement de S, K, I, T, F?

Note rapide, j'autorise le polymorphisme paramétrique (système F) dans ce système afin que S, Ket Ipuisse fonctionner sur tous les types.

Notez que sans correspondance de motif, nous ne pouvons pas écrire ifquoi que nous fassions. Nous n'avons absolument aucune opération sur les booléens. Il n'y a pas moyen de distinguer Truede False. Essayez plutôt

true : a -> a -> a
true = \t -> \f -> t

false : a -> a -> a
false = \t -> \f -> f

Laissons Bool = a -> a -> apour plus de clarté.

 if : Bool -> a -> a -> a
 if = \bool -> \a -> \b -> bool a b

Il ne reste plus qu'à compiler des expressions de calcul lambda dans des combinateurs, ce qui est assez trivial.

if : Bool -> a -> a -> a -- Or just Bool -> Bool
if    = I

true : a -> a -> a
true  = K

false : a -> a -> a
false = K I