firmas/tipos en programación funcional (OCaml)

Question

Empecé a aprender programación funcional (OCaml), pero no entiendo un tema importante sobre fp: firmas (no estoy seguro de si es un nombre propio). Cuando escribo algo y compilar con ocaml, que consigo por ejemplo:

# let inc x = x + 1 ;; 
val inc : int -> int = <fun> 

Esto es trivial, pero no sé, ¿por qué esto:

let something f g a b = f a (g a b) 

da una salida:

val something : (’a -> ’b -> ’c) -> (’a -> ’d -> ’b) -> ’a -> ’d -> ’c = <fun> 

Supongo que este tema es absolutamente básico para muchos de ustedes, pero pido ayuda aquí, porque no he encontrado nada en Internet sobre firmas en OCaml (hay algunos artículos sobre firmas en Haskell, pero no explicaciones).

Si este tema de alguna manera va a sobrevivir, he puesto aquí varias funciones, que las firmas hechas me confunde:

# let nie f a b = f b a ;; (* flip *) 
val nie : (’a -> ’b -> ’c) -> ’b -> ’a -> ’c = <fun> 

# let i f g a b = f (g a b) b ;; 
val i : (’a -> ’b -> ’c) -> (’d -> ’b -> ’a) -> ’d -> ’b -> ’c = <fun> 


# let s x y z = x z (y z) ;; 
val s : (’a -> ’b -> ’c) -> (’a -> ’b) -> ’a -> ’c = <fun> 

# let callCC f k = f (fun c d -> k c) k ;; 
val callCC : ((’a -> ’b -> ’c) -> (’a -> ’c) -> ’d) -> (’a -> ’c) -> ’d = <fun> 

darle las gracias por la ayuda y explicación.

Answer 1

Hay un par de conceptos que usted necesita entender para dar sentido a este tipo de firma y no sé cuáles ya lo hacen, así que hice mi mejor esfuerzo para explicar cada concepto importante:

Currying

Como usted sabe, si tiene el tipo foo -> bar, esto describe una función que toma un argumento de tipo foo y devuelve un resultado del tipo bar. Dado que -> es asociativo correcto, el tipo foo -> bar -> baz es el mismo que foo -> (bar -> baz) y describe así una función tomando un argumento del tipo foo y devolviendo un valor de tipo bar -> baz, lo que significa que el valor devuelto es una función tomando un valor del tipo bar y devolviendo un valor del tipo baz.

Tal función puede ser llamada como my_function my_foo my_bar, que por aplicación de función se deja-asociativa, es el mismo que (my_function my_foo) my_bar, es decir, se aplica my_function al argumento my_foo y luego se aplica la función que se devuelve como resultado al argumento my_bar.

Como se puede llamar así, una función del tipo foo -> bar -> baz a menudo se denomina "una función que toma dos argumentos" y lo haré en el resto de esta respuesta.

variables de tipo

Si se define una función como let f x = x, tendrá el tipo 'a -> 'a. Pero 'a no es realmente un tipo definido en la biblioteca estándar OCaml, entonces, ¿qué es?

Cualquier tipo que comience con ' es una variable de tipo llamada . Una variable de tipo puede representar cualquier tipo posible. Por lo tanto, en el ejemplo anterior, se puede llamar al f con un int o un string o un list o cualquier cosa, no importa.

Además, si la misma variable de tipo aparece en una firma de tipo más de una vez, representará el mismo tipo. Entonces, en el ejemplo anterior, eso significa que el tipo de devolución de f es el mismo que el tipo de argumento. Por lo tanto, si se llama a f con un int, devuelve un int. Si se llama con un string, devuelve un string y así sucesivamente.

Así que una función de tipo 'a -> 'b -> 'a podría tomar dos argumentos de cualquier tipo (que podría no ser del mismo tipo para el primer y segundo argumento) y devolvería un valor del mismo tipo que el primer argumento, mientras que una función de tipo 'a -> 'a -> 'a tomaría dos argumentos del mismo tipo.

Una nota sobre la inferencia de tipo: A menos que especifique explícitamente una función como una firma de tipo, OCaml siempre deducirá el tipo más general posible para usted. Entonces, a menos que una función use cualquier operación que solo funcione con un tipo dado (como + por ejemplo), el tipo inferido contendrá variables de tipo.

Ahora, para explicar el tipo ...

val something : ('a -> 'b -> 'c) -> ('a -> 'd -> 'b) -> 'a -> 'd -> 'c = <fun> 

Este tipo de firma que dice que something es una función de tomar cuatro argumentos.

El tipo del primer argumento es 'a -> 'b -> 'c. Es decir. una función que toma dos argumentos de tipos arbitrarios y posiblemente diferentes y devuelve un valor de un tipo arbitrario.

El tipo del segundo argumento es 'a -> 'd -> 'b. Esta es nuevamente una función con dos argumentos. Lo importante a tener en cuenta aquí es que el primer argumento de la función debe tener el mismo tipo que el primer argumento de la primera función y el valor de retorno de la función debe tener el mismo tipo que el segundo argumento de la primera función.

El tipo del tercer argumento es 'a, que también es el tipo de los primeros argumentos de ambas funciones.

Por último, el tipo del cuarto argumento es 'd, que es el tipo del segundo argumento de la segunda función.

El valor de retorno será del tipo 'c, es decir, el tipo de retorno de la primera función.

Answer 2

Si está realmente interesado en el tema (y tiene acceso a una biblioteca de la universidad), lea la excelente (aunque algo anticuada) "Introducción a la programación funcional" de Wadler. Explica las firmas de tipo y la inferencia de tipos de una manera muy agradable y legible. más

Dos consejos: Tenga en cuenta que la flecha -> es asociativo por la derecha, por lo que puede poner entre paréntesis las cosas desde la derecha que a veces ayuda a entender las cosas, es decir a -> b -> c es lo mismo que a -> (b -> c). Esto está conectado a la segunda sugerencia: funciones de orden superior. Puede hacer cosas como

let add x y = x + y 
let inc = add 1 

por lo que en FP, pensando en 'añadir' como una función que tiene que tomar dos parámetros numéricos y devuelve un valor numérico es generalmente no lo que hay que hacer: también puede ser una función que toma un argumento numérico y devuelve una función con tipo num -> num.

Comprender esto lo ayudará a comprender las firmas de tipo, pero puede hacerlo sin él. Aquí, rápido y fácil:

# let s x y z = x z (y z) ;; 
val s : (’a -> ’b -> ’c) -> (’a -> ’b) -> ’a -> ’c = <fun> 

Mire a la derecha. y tiene un argumento, por lo que es del tipo a -> b donde a es el tipo de z. x tiene dos argumentos, el primero de los cuales es z, por lo que el tipo del primer argumento también debe ser a. El tipo de (y z), el segundo argumento, es b y, por lo tanto, el tipo de x es (a -> b -> c). Esto le permite deducir el tipo de s inmediatamente.