Como hay un cálculo lambda sin tipo y un cálculo lambda de tipo simple (como se describe, por ejemplo, en el libro Tipos y lenguajes de programación de Benjamin Pierce), ¿existe una lógica combinatoria de tipo simple?
Por ejemplo, parecería que los tipos naturales para los combinadores S, K y yo serían
S : (a -> b -> c) -> (a -> b) -> a -> c
K : a -> b -> a
I : a -> a
donde a, byc son variables de tipo que se extienden sobre un conjunto de tipos T. Ahora, quizás podríamos comenzar con un solo tipo base, Bool. Nuestro conjunto de tipos T es Bool junto con cualquier tipo que se pueda formar usando los tres patrones
(a -> b -> c) -> (a -> b) -> a -> c
a -> b -> a
a -> a
donde a, b, c en T.
Habría dos constantes nuevas en el idioma.
T : Bool
F : Bool
Entonces, este lenguaje consiste en los símbolos S, K, I, T y F, junto con paréntesis. Tiene un tipo base Bool, y los "tipos de función" que se pueden hacer a partir de los patrones de combinador S, K e I.
¿Se puede hacer que este sistema funcione? Por ejemplo, ¿hay una construcción de tipo si-entonces-otro bien tipada que se pueda formar solo con S, K, I, T, F?
fuente
Respuestas:
Nota rápida, que permita que el polimorfismo paramétrico (Sistema F) en este sistema para que
S
,K
yI
puede trabajar sobre todo tipo.Tenga en cuenta que sin la coincidencia de patrones, no podemos escribir un
if
no importa lo que hagamos. No tenemos absolutamente ninguna operación en booleanos. No hay forma de distinguirTrue
deFalse
. En su lugar, intenteDejemos la
Bool = a -> a -> a
claridad.Ahora es solo cuestión de compilar algunas expresiones de cálculo lambda en combinadores, lo cual es bastante trivial.
fuente