Determinación del tipo de una función en Programación funcional

Question

Las siguientes ecuaciones están escritas en Miranda Syntax, pero debido a las similitudes entre Miranda y Haskell, ¡supongo que los programadores de Haskell deberían entenderlo!

Si define las siguientes funciones:

rc v g i = g (v:i) 
rn x = x 
rh g = hd (g []) 


f [] y = y 
f (x:xs) y = f xs (rc x y) 

g [] y = y 
g (x:xs) y = g xs (x:y) 

¿Cómo se calcula el tipo de las funciones? Creo que entiendo cómo resolverlo para f, g y rn, pero estoy confundido acerca de la parte de la aplicación parcial.

rn va a ser * -> * (o cualquier cosa -> nada, yo creo que es un -> a en Haskell)

para F y G, son los tipos de funciones tanto [*] -> * -> *?

No estoy seguro de cómo encontrar los tipos de rc y rh. En rc, g se aplica parcialmente a la variable i, así que supongo que esto limita el tipo de i a ser [*]. ¿Qué orden se aplica rc yg en la definición de rc? ¿Se aplica g a i, y luego la función resultante se usa como argumento para rc? ¿O toma rc 3 parámetros separados de v, g e i? Estoy realmente confundido ... ¡cualquier ayuda sería apreciada! Gracias chicos.

Lo sentimos olvidó añadir que el HD es la función de la cabeza estándar para una lista y se define como:

hd :: [*] -> * 
hd (a:x) = a 
hd [] = error "hd []" 

Answer 1

El tipo se infiere de lo que ya se sabe de tipos y cómo se utilizan las expresiones en la definición.

Vamos a empezar en la parte superior,

rc v g i = g (v : i) 

por lo rc :: a -> b -> c -> d y hay que ver lo que se puede encontrar a cabo sobre a, b, c y d. En el lado derecho, aparece (v : i), por lo que con v :: a, vemos que i :: [a], c = [a]. A continuación, se aplica a gv : i, por lo g :: [a] -> d, en conjunto,

rc :: a -> ([a] -> d) -> [a] -> d 

rn x = x significa que no hay ninguna restricción sobre el tipo de argumento de rn y su tipo de retorno es el mismo, rn :: a -> a.

rh g = hd (g []) 

Desde rh 's argumento g se aplica a una lista vacía en el lado derecho, se debe tener un tipo [a] -> b, posiblemente más información sobre a o b siguiente. De hecho, g [] es el argumento de hd en el lado derecho, por lo g [] :: [c] y g :: [a] -> [c], por lo tanto,

rh :: ([a] -> [c]) -> c 

Siguiente

f [] y = y 
f (x:xs) y = f xs (rc x y) 

El primer argumento es una lista, y si eso es vacía, el resultado es el segundo argumento, por lo que f :: [a] -> b -> b se sigue de la primera ecuación.Ahora, en la segunda ecuación, en el RHS, el segundo argumento para f es rc x y, por lo tanto rc x y debe tener el mismo tipo que y, lo llamamos b. Pero

rc :: a -> ([a] -> d) -> [a] -> d 

, entonces b = [a] -> d. Por lo tanto

f :: [a] -> ([a] -> d) -> [a] -> d 

Finalmente

g [] y = y 
g (x:xs) y = g xs (x:y) 

de la primera ecuación deducimos g :: [a] -> b -> b. A partir del segundo, deducimos b = [a], ya que tomamos la cabeza del primer argumento y los contras de TI g 's para el segundo, por lo tanto

g :: [a] -> [a] -> [a] 

Answer 2

Voy a usar la sintaxis de Haskell para escribir tipos.

rc v g i = g (v:i) 

Aquí rc toma tres parámetros, por lo que su tipo será algo así como a -> b -> c -> d. v:i debe ser una lista de elementos del mismo tipo que v y i, entonces v :: a y i :: [a]. g se aplica a esa lista, por lo que g :: [a] -> d. Si junta todo, obtiene rc :: a -> ([a] -> d) -> [a] -> d.

Como ya descubrió rn :: a -> a, porque es simplemente la identidad.

No tengo idea sobre el tipo de la función hd que usa en rh, así que me saltearé eso.

f [] y = y 
f (x:xs) y = f xs (rc x y) 

Aquí f toma dos parámetros, por lo que su tipo será algo así como a -> b -> c. Del primer caso podemos deducir que b == c, ya que devolvemos y, y que el primer argumento es una lista. Por ahora sabemos que f :: [a'] -> b -> b. En el segundo caso la notificación cómo x y y se dan en la entrada a rc: y debe ser una función [a'] -> d, y rc x y :: a' -> d (que debe ser también el tipo de y, ya que se pasa como segundo argumento de f). Finalmente, podemos decir que f :: [a'] -> ([a'] -> d) -> ([a'] -> d). Dado que -> es asociativo de la derecha, esto es equivalente a [a'] -> ([a'] -> d) -> [a'] -> d.

Puede razonar de la misma manera para los restantes.