El tipo de firma de un combinador no coincide con la firma de tipo de su función Lambda equivalente

Question

consideran este combinador:

S (S K) 

aplicarlo a los argumentos XY:

S (S K) X Y 

Se contrae a:

X Y 

Convertí S (SK) a los términos Lambda correspondientes y obtuve este resultado:

(\x y -> x y) 

he utilizado la herramienta de Haskell WinGHCi para obtener la firma de tipo de (\ x y -> x, y) y ha devuelto:

(t1 -> t) -> t1 -> t 

que tenga sentido para mí.

A continuación, utiliza WinGHCi para obtener la firma de tipo de s (s k) y ha devuelto:

((t -> t1) -> t) -> (t -> t1) -> t 

Eso no tiene sentido para mí. ¿Por qué las firmas de tipos son diferentes?

Nota: I definió s, k, y yo como:

s = (\f g x -> f x (g x)) 
k = (\a x -> a) 
i = (\f -> f) 

Answer 1

Gracias a todos los que respondieron a mi pregunta. He estudiado tus respuestas. Para estar seguro de entender lo que aprendí, escribí mi propia respuesta a mi pregunta. Si mi respuesta no es correcta, házmelo saber.

empezamos con los tipos de k y s: primer trabajo

k :: t1 -> t2 -> t1 
    k = (\a x -> a) 

    s :: (t3 -> t4 -> t5) -> (t3 -> t4) -> t3 -> t5 
    s = (\f g x -> f x (g x)) 

Vamos en determing la firma tipo de (s k).

Recall s 's definición:

s = (\f g x -> f x (g x)) 

Sustituyendo k para f resultados en (\f g x -> f x (g x)) contratación a:

(\g x -> k x (g x)) 

Importante El tipo de g y x debe ser consistente con k' s escriba la firma.

Recordemos que k tiene este tipo de firma:

k :: t1 -> t2 -> t1 

Por lo tanto, para esta definición de la función k x (g x) podemos inferir:

• El tipo de x es el tipo de primer argumento k 's , que es el tipo t1.

• El tipo de segundo argumento k 's es t2, por lo que el resultado de (g x) debe ser t2.

• g tiene x como su argumento que ya hemos determinado tiene el tipo t1. Por lo tanto, la firma de tipo (g x) es (t1 -> t2).

• El tipo de resultado k 's es t1, por lo que el resultado de (s k) es t1.

Por lo tanto, el tipo de firma de (\g x -> k x (g x)) es la siguiente:

(t1 -> t2) -> t1 -> t1 

A continuación, k se define para volver siempre su primer argumento.Así que esto:

k x (g x) 

contratos a esto:

x 

Y esto:

(\g x -> k x (g x)) 

contratos a esto:

(\g x -> x) 

Bien, ahora se han dado cuenta (s k) :

s k :: (t1 -> t2) -> t1 -> t1 
    s k = (\g x -> x) 

Ahora determinemos el tipo de firma de s (s k).

Procedimos de la misma manera.

Recall s 's definición:

s = (\f g x -> f x (g x)) 

Sustituyendo (s k) para f resultados en (\f g x -> f x (g x)) contratante:

(\g x -> (s k) x (g x)) 

Importante El tipo de g y x debe ser consistente con (s k)' s escriba la firma.

Recordemos que (s k) tiene este tipo de firma:

s k :: (t1 -> t2) -> t1 -> t1 

Por lo tanto, para esta definición de la función (s k) x (g x) podemos inferir:

• El tipo de x es el tipo de primer argumento (s k) 's , que es el tipo (t1 -> t2).

• El tipo de segundo argumento (s k) 's es t1, por lo que el resultado de (g x) debe ser t1.

• g tiene x como su argumento, que ya hemos determinado tiene el tipo (t1 -> t2). Entonces la firma de tipo de (g x) es ((t1 -> t2) -> t1).

• El tipo de resultado (s k) 's es t1, por lo que el resultado de s (s k) es t1.

Por lo tanto, el tipo de firma de (\g x -> (s k) x (g x)) es la siguiente:

((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 

Anteriormente hemos determinado que s k tiene esta definición:

(\g x -> x) 

Es decir, se trata de una función que toma dos argumentos y devuelve el segundo.

Por lo tanto, la siguiente:

(s k) x (g x) 

contratos a esto:

(g x) 

Y esto:

(\g x -> (s k) x (g x)) 

contratos a esto:

(\g x -> g x) 

Bien, ahora nos hemos dado cuenta s (s k).

s (s k) :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 
    s (s k) = (\g x -> g x) 

Por último, comparar la firma tipo de s (s k) con la firma tipo de esta función:

p = (\g x -> g x) 

El tipo de p es:

p :: (t1 -> t) -> t1 -> t 

p y s (s k) tienen la misma definición (\g x -> g x) entonces ¿por qué tienen diferentes tipos de firmas?

La razón por la que s (s k) tiene una firma de tipo diferente a p es que no hay restricciones en p. Vimos que el s en (s k) está obligado a ser coherente con la firma de tipo k, y el primer s en s (s k) está obligado a ser coherente con la firma de tipo (s k). Por lo tanto, la firma de tipo s (s k) está restringida debido a su argumento. Aunque p y s (s k) tienen la misma definición, las restricciones en g y x son diferentes.

Answer 2

Empezamos con los tipos de k y s

k :: t1 -> t2 -> t1 
k = (\a x -> a) 

s :: (t3 -> t4 -> t5) -> (t3 -> t4) -> t3 -> t5 
s = (\f g x -> f x (g x)) 

Así pasa k como primer argumento de s, nos unificar el tipo de k con el tipo del primer argumento de s y usar s en el tipo

s :: (t1 -> t2 -> t1) -> (t1 -> t2) -> t1 -> t1 

por lo tanto obtenemos

s k :: (t1 -> t2) -> t1 -> t1 
s k = (\g x -> k x (g x)) = (\g x -> x) 

Luego, en s (s k), el exterior s se utiliza en el tipo (t3 = t1 -> t2, t4 = t5 = t1)

s :: ((t1 -> t2) -> t1 -> t1) -> ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 

aplicación que a s k gotas del tipo del primer argumento y nos deja con

s (s k) :: ((t1 -> t2) -> t1) -> (t1 -> t2) -> t1 

Como resumen: en Haskell, el tipo de s (s k) se deriva de los tipos de sus subexpresiones constituyentes, no de su efecto sobre su (s) argumento (s). Por lo tanto, tiene un tipo menos general que la expresión lambda que denota el efecto de s (s k).

Answer 3

El sistema de tipos que está utilizando es básicamente el mismo que el cálculo lambda simplemente tipado (no está utilizando ninguna función recursiva o recursiva). El cálculo lambda simplemente tipado no es completamente general; no es Turing-completo, y no puede usarse para escribir recursividad general.El cálculo del combinador SKI es Turing-completo, y puede usarse para escribir combinators de punto fijo y recursión general; por lo tanto, la potencia máxima del cálculo combinador SKI no puede expresarse en cálculo lambda de tipo simple (aunque puede ser en cálculo lambda no tipificado).