haskell - Tipo de diversión gx=ys donde ys=[x]++ filter(curry gx) ys?

types unification

Question

Estoy tratando de entender por qué el tipo de fun gx = ys where ys = [x] ++ filter (curry gx) ys es ((a, a) -> Bool) -> a -> [a] .

Entiendo que:

filter :: (a -> Bool) -> [a] -> [a] y ese curry :: ((a, b) -> c) -> a -> b -> c

Pero no entiendo cómo continuar.

Answer 1

El siguiente enfoque no es necesariamente el más fácil ni el más rápido, pero es relativamente sistemático.

Estrictamente hablando, estás buscando el tipo de

/g -> (/ x -> let ys = (++) [x] (filter (curry g x) ys) in ys)

( let y where son equivalentes, pero a veces es un poco más fácil razonar usando let ), dados los tipos

filter :: (a -> Bool) -> [a] -> [a]
curry :: ((a, b) -> c) -> a -> b -> c

No olvides que también estás usando

(++) :: [a] -> [a] -> [a]

Primero veamos la parte más "profunda" del árbol de sintaxis:

curry g x

Tenemos x , de los cuales no hemos visto antes todavía, así que asumiremos que tienen algún tipo:

g :: t1
x :: t2

También tenemos curry . En cada punto donde se producen estas funciones, las variables de tipo ( a , b , c ) se pueden especializar de forma diferente, por lo que es una buena idea reemplazarlas por un nombre nuevo cada vez que utilice estas funciones. En este punto, curry tiene el siguiente tipo:

curry :: ((a1, b1) -> c1) -> a1 -> b1 -> c1

Entonces solo podemos decir curry gx si los siguientes tipos se pueden unificar:

t1  ~  ((a1, b1) -> c1)       -- because we apply curry to g
t2  ~  a1                     -- because we apply (curry g) to x

Entonces también es seguro suponer que

g :: ((a1, b1) -> c1)
x :: a1
---
curry g x :: b1 -> c1

Continuemos:

filter (curry g x) ys

Vemos ys por primera vez, así que vamos a mantenerlo en ys :: t3 por ahora. También tenemos que instanciar el filter . Entonces, en este punto, sabemos

filter :: (a2 -> Bool) -> [a2] -> [a2]
ys :: t3

Ahora debemos hacer coincidir los tipos de argumentos del filter :

b1 -> c1  ~  a2 -> Bool
t3        ~  [a2]

La primera restricción se puede desglosar para

b1  ~  a2
c1  ~  Bool

Ahora sabemos lo siguiente:

g :: ((a1, a2) -> Bool)
x :: a1
ys :: [a2]
---
filter (curry g x) ys :: [a2]

Continuemos.

(++) [x] (filter (curry g x) ys)

No dedicaré demasiado tiempo a explicar [x] :: [a1] , veamos el tipo de (++) :

(++) :: [a3] -> [a3] -> [a3]

Obtenemos las siguientes limitaciones:

[a1]  ~  [a3]           -- [x]
[a2]  ~  [a3]           -- filter (curry g x) ys

Dado que estas restricciones se pueden reducir a

a1  ~  a3
a2  ~  a2

llamaremos a todos estos a a1 :

g :: ((a1, a1) -> Bool)
x :: a1
ys :: [a1]
---
(++) [x] (filter (curry g x) ys) :: [a1]

Por ahora, voy a ignorar que el tipo ys se generaliza y me enfoco en

/x -> let { {- ... -} } in ys

Sabemos qué tipo necesitamos para x , y sabemos el tipo de ys , entonces ahora sabemos

g :: ((a1, a1) -> Bool)
ys :: [a1]
---
(/x -> let { {- ... -} } in ys) :: a1 -> [a1]

De manera similar, podemos concluir que

(/g -> (/x -> let { {- ... -} } in ys)) :: ((a1, a1) -> Bool) -> a1 -> [a1]

En este punto, solo tiene que cambiar el nombre (en realidad, generalizar, porque desea vincularlo a la fun ) las variables de tipo y tiene su respuesta.

Answer 2

Podemos derivar tipos en Haskell de una manera más o menos mecánica, utilizando el esquema general de

foo      x =  y                              -- is the same as
foo   = /x -> y                              -- so the types are
foo   :: a -> b          , x :: a , y :: b   -- so that
foo      x :: b                              

lo que significa que, por ejemplo

f    x    y    z :: d    , x :: a , y :: b, z :: c

implica

f    x    y :: c -> d
f    x :: b -> c -> d
f :: a -> b -> c -> d

Con estos simples trucos, la derivación del tipo será trivial para ti. Adjunto

filter :: (a -> Bool) -> [a] -> [a]  
curry  :: ((a, b) -> c) -> a -> b -> c
(++)   :: [a] -> [a] -> [a]

simplemente escribimos las cosas cuidadosamente alineadas, procesándolas de arriba hacia abajo , renombrando y sustituyendo constantemente las variables de tipo, y registrando las equivalencias de tipo en el costado:

fun    g    x = ys   where   ys = [x] ++ filter (curry g x) ys 
fun    g    x :: c              , ys :: c
fun    g :: b -> c              , x  :: b 
fun :: a -> b -> c              , g  :: a 

ys = [x] ++ filter (curry g x) ys c ~ c (++) [x] (filter (curry g x) ys) :: c (++) :: [a1] -> [a1] -> [a1] ----------------------------------------------- (++) :: [b] -> [b] -> [b] , a1 ~ b , c ~ [b] filter (curry g x ) ys :: [b] filter :: (a2 -> Bool) -> [a2] -> [a2] , a2 ~ b -------------------------------------- filter :: (b -> Bool) -> [b] -> [b] curry g x :: b -> Bool curry :: ((a3, b) -> c3 ) -> a3 -> b -> c3 , c3 ~ Bool , a3 ~ b ------------------------------------------- curry :: ((b , b) -> Bool) -> b -> b -> Bool , a ~ ((b,b) -> Bool)

entonces tenemos eso a ~ ((b,b) -> Bool) y c ~ [b] , y por lo tanto

fun :: a               -> b ->  c
fun :: ((b,b) -> Bool) -> b -> [b]

que es lo mismo que ((a,a) -> Bool) -> a -> [a] , hasta un cambio de nombre consistente de variables de tipo.