Teniendo una función de Haskell como ‘dos ​​veces fx = f (fx)’, ¿cuál es la regla que puedo aplicar para obtener su tipo (sin HUGS o similar)?

Answer 1

El razonamiento sobre las firmas de tipo es una habilidad que solo proviene de la lectura / escritura de código funcional (ya que las funciones en FP tienden a tener firmas de tipo más complejas debido al polimorfismo incorporado).

Un buen consejo para comenzar es utilizar nuevas variables de tipo para las partes de la firma de las que no conoce el tipo. Por ejemplo, tanto f como x en dos veces fx = f (fx) tienen tipos polimórficos, ya que no hay nada en el cuerpo de la función que restrinja el tipo (como esto def: twicePlusOne fx = f (fx) + 1 , donde el el tipo de retorno está restringido a ser de tipo Int ). Entonces, usando variables de tipo fresco (generalmente comenzando con a, b, c… (o sus equivalentes griegos), podemos razonar sobre la firma de f como (a -> a) , ya que en el cuerpo de dos veces f simplemente toma un argumento para devolver un resultado Y el resultado debe ser del mismo tipo que el tipo de argumento de f ya que f se aplica directamente al resultado de (fx) . Dado que hemos establecido que el tipo de argumento de f debe ser a , podemos deducir que el tipo de x también debe ser a , ya que estamos aplicando f a x .

Se nos ocurrió lo siguiente:
         
f :: (a -> a)
x :: a

y como un resultado

dos veces :: (a -> a) -> a ->?

Lo último que queda por descubrir es el tipo de retorno de la función dos veces . Esto es bastante simple de deducir ya que conocemos el tipo de retorno de f ; El valor de retorno de la función dos veces se calcula aplicando f , por lo que la función dos veces debe tener el mismo tipo de retorno que f. Esto produce la siguiente firma de tipo dos veces:

dos veces :: (a -> a) -> a -> a

Espero que haya sido fácil de seguir, ya que describe cómo podría razonar sobre las firmas de tipo polimórfico.

Answer 2

No sé acerca de una regla, per se, pero solo pensarla dará la respuesta. Por supuesto, en realidad no necesita saber el tipo la mayor parte del tiempo, ya que Haskell puede descubrir la mayoría de los tipos.

Primero, pensemos en el tipo de f . Obviamente tiene que tomar un argumento, y tiene que devolver algo.

Entonces obtenemos un tipo de, porque los tipos podrían ser diferentes:

f :: a -> b

La función tiene que aceptar twice la función, un argumento del tipo a (porque tiene que ser válida cuando se llama a f con el argumento), y devuelve un valor del tipo b , porque su resultado se obtiene mediante el uso de f que devuelve a b . Entonces:

twice :: (a -> b) -> a -> b

Sin embargo, debido a que f se aplica al resultado de una aplicación de sí mismo, eso significa que b debe ser un argumento válido para f , en otras palabras, a ~ b , es decir, son lo mismo. Entonces, realmente, podemos reemplazar todos a y b con el mismo tipo, lo llamaré t para no ser confuso, y obtenemos:

twice :: (t -> t) -> t -> t

Y, de hecho, si ghci en ghci y lo pregunto, de hecho me dice:

Answer 3

Piense en descifrar el tipo como un problema de restricción-satisfacción . Comience con las entradas siendo lo más generales posible (es decir, f :: a ) y luego reduzca el tipo en función de cómo se usa f . Después de un poco de práctica y la experiencia de Haskell, comenzará a hacerlo intuitivamente y omitirá los pasos, pero es un buen lugar para comenzar, ¡y no muy lejos de cómo funciona el algoritmo de inferencia de tipos real!

¿Cómo sería eso para tu ejemplo? Bueno, tenemos dos entradas:

f :: a, x :: b

Luego comenzamos a trabajar desde la parte más interna de la expresión fx . ¿Qué nos dice esto sobre x ? Nada. ¿Qué nos dice sobre f ? f tiene que ser una función que acepte x . Ahora sabemos un poco más:

f :: b -> c, x :: b

Ahora la siguiente capa de la expresión: f (fx) . Usando lo que sabemos de f hasta ahora , esta tiene que ser una función c -> d . Pero esto es diferente de b -> c , que teníamos antes. ¿Hay alguna forma de asignar b, c, d modo que b -> c y c -> d sean iguales? ¡Si! Podemos ponerlos a todos a b . Esto nos da:

f :: b -> b, x :: b

Finalmente, podemos juntar todo esto para obtener el tipo de la función completa:

dos veces :: (b -> b) -> b -> b

Estrictamente, probablemente omití algunos pasos, pero usted tiene la idea general: comience con variables generales y luego acórtelas usando la expresión como un conjunto de restricciones .

Answer 4

En realidad: hay algunos tipos diferentes posibles para esta función, pero el que HUGS y GHC obtienen automáticamente es el más simple.

dos veces :: a -> b -> c – porque hay tres argumentos
a = d -> e – porque es una función
e = d – porque el resultado de ‘f x’ también es un argumento adecuado para ‘f’
d = b – porque el segundo argumento se aplica a ‘f’
dos veces :: (b -> b) -> b -> b – sustituyendo todo nuevamente en el tipo original
dos veces :: (a -> a) -> a -> a – cambie el nombre de la variable de tipo restante.

Si está utilizando la extensión de lenguaje RankNTypes, puede especificar manualmente otros tipos para la función siempre que sean coherentes con la definición. Por ejemplo:

dos veces :: para a. (para todos los b. b -> [b]) -> a -> [[a]]

Answer 5

Todos los operadores de composición como f . g f . g implica que el tipo en la salida de la función en el lado derecho ( g ) debe coincidir con la entrada de la función en el lado izquierdo ( f ). Sin embargo, dado que en su condición ambas son las mismas funciones f , simplemente podemos razonar que la función f toma y devuelve el mismo tipo. Entonces el tipo compuesto debería ser

t -> t