Duda de tipos

Duda de tipos

de Veronica Dahiana Bentancor Cedrez -
Número de respuestas: 6

Buenas, no estoy pudiendo calcular el tipo de:   flip foldr id


El tipo de foldr para el curso es (a->b->b)->b->[a]->b,

Empece por calcular el tipo de flip foldr y creía que debería tener tipo  (a->b->b)->[a]->b->b, (ya que intercambiaría el neutro por la lista) 

sin embargo el tipo es b -> (a -> b -> b) -> [a] -> b


Gracias, saludos!

En respuesta a Veronica Dahiana Bentancor Cedrez

Re: Duda de tipos

de Marcos Viera - InCo -

El tipo de flip es:

flip :: (t1 -> t2 -> t3) -> t2 -> t1 -> t3

o sea que toma una función que toma dos parámetros y retorna una función que toma los dos parámetros intercambiados.

El tipo de foldr es:

foldr :: (a -> b -> b) -> b -> [a] -> b

como la -> asocia a la derecha podemos agregar los siguientes paréntesis sin cambiar nada:

foldr :: (a -> b -> b) -> b -> ([a] -> b)
entonces podemos ver que si foldr es la función que le pasamos a flip, tenemos:
t1 = (a -> b -> b)
t2 = b
t3 = ([a] -> b)

Entonces el resultado de la aplicación del flip, que es de tipo t2 -> t1 -> t3, quedaría:

flip foldr :: b -> (a -> b -> b) -> ([a] -> b)

o lo que es lo mismo:

flip foldr :: b -> (a -> b -> b) -> [a] -> b



En respuesta a Marcos Viera - InCo

Re: Duda de tipos

de Gaston Daniel Barreto Sugliani -

Hola Marcos,

Cómo haces por ejemplo cuando tenes que hacer coincidir una tupla con algo que no es una tupla?

Por ejemplo para  curry . curry

curry . curry :: (((a, b1), b2) -> c) -> a -> b1 -> b2 -> c


curry :: ((t1, t2) -> t3) -> t1 -> t2 -> t3
curry :: ((a, b) -> c) -> a -> b -> c

como hallas el tipo de t1, t2?

En respuesta a Gaston Daniel Barreto Sugliani

Re: Duda de tipos

de Marcos Viera - InCo -

Para desambiguar, digamos que el curry de la izquierda tiene tipo:

curry :: ((t1, t2) -> t3) -> t1 -> t2 -> t3

el de la derecha:

curry :: ((a, b) -> c) -> a -> b -> c

y la composición:

(.) :: (t' -> t'') -> (t -> t') -> t -> t''


entonces al hacer curry . curry sabemos:

- por el primer curry que aplico a la composición:

t' = ((t1, t2) -> t3)

t'' = t1 -> t2 -> t3

- por el segundo curry que aplico a la composición:

t = ((a, b) -> c)

t' = a -> b -> c

sobre t' sé:

t' = ((t1, t2) -> t3) = a -> b -> c

entonces:

(t1,t2) = a 

t3 = b -> c 

Finalmente puedo decir que:

t = (((t1,t2),b) -> c)

t'' = t1 -> t2 -> b -> c

Entonces:

curry . curry :: (((t1,t2),b) -> c)  -> t1 -> t2 -> b -> c

Como verán, cada vez que igualo una variable con algo más explícito, me quedo con lo más explícito.


En respuesta a Marcos Viera - InCo

Re: Duda de tipos

de Veronica Dahiana Bentancor Cedrez -

Hola, con respecto al tipo de flip foldr id, aun no he logrado calcularlo....

Pensaba calcular el tipo de foldr id y luego el de flip de eso, pero me di cuenta que de ese modo estoy calculando el tipo de flip(foldr id) que no es el mismo de flip foldr id.

Volvinedo al flip foldr id, el flip hará que intercambie de el neutro con la lista para el foldr? o lo estoy interpretando mal?

Como se calcula el tipo en estos casos de varias funciones? No me queda muy claro por donde comenzar.


Gracias

En respuesta a Veronica Dahiana Bentancor Cedrez

Re: Duda de tipos

de Juan Pablo García Garland -

La aplicación asocia a la izquierda así que como bien habías observado, las expresiones flip foldr id y (flip foldr) id son equivalentes.

Como explicó Marcos más arriba

flip foldr :: b → (a → b → b) → [a] → b

porque flip intercambia los primeros dos argumentos. Este tipo es polimórfico, pensá que existen instancias de flip foldr para par de tipos a y b posibles. Estos tipos pueden ser monomórficos, o no.

Por ejemplo Bool → (Int → Bool → Bool) → [Int] → Bool es una instancia de tipo para flip foldr (hacemos [b:= Char, a:=Int]). Por otro lado (c → c) → (a → (c → c) → (c → c)) → [a] → (c → c) también es una instancia (hacemos [b:= c → c], es decir, b sique siendo polimórfico, pero no es cualquier cosa, sabemos que es una función de un tipo en sí mismo).

Cuando haacemos la aplicación para obtenerflip foldr id, consumimos argumento (el b en el tipo original), pero como id tiene tipo c → c (de nuevo uso la variable c para que sea fresca), entonces necesitamos la instancia de flip foldr adecuada (la más general posible, pero sabiendo que b era en realidad de la forma c → c), que es la anterior ((c → c) → ( a → (c → c) → (c → c)) → [a] → (c → c)).

Entonces queda flip foldr id :: (a → (c → c) → (c → c)) → [a] → (c → c)