Explicación de la aplicación parcial - join

Question

¿Por qué funciona la aplicación parcial de funciones con diferentes firmas?

Tome Control.Monad.join como ejemplo:

GHCi> :t (=<<) 
(=<<) :: Monad m => (a -> m b) -> m a -> m b 
GHCi> :t id 
id :: a -> a 
GHCi> :t (=<<) id 
(=<<) id :: Monad m => m (m b) -> m b 

¿Por qué se acepta id :: a -> a en lugar de (a -> m b) argumento, ya que son obviamente diferentes?

Answer 1

=<< 's type signature dice que el primer argumento es una función de a (cualquier cosa) a una mónada de b.

Bueno, m b cuenta como cualquier cosa, ¿verdad? Así que sólo podemos sustituir en m b para cada a:

(=<<) :: Monad m => (m b -> m b) -> m (m b) -> m b 

id s tipo dice que es una función de cualquier cosa a la misma cosa. Así que si tenemos en sub m b (sin olvidar la restricción mónada), obtenemos:

id :: Monad m => m b -> m b 

A continuación se puede ver que el partido de tipos.

Answer 2

Se trata de unificar a con m b, y simplemente decide que debe haber am b, por lo que el tipo de (bajo el supuesto de a ~ m b) es Monad m => (mb -> m b) -> m (m b) -> m b, y una vez que lo aplica a id, aún le quedan Monad m => m (m b) -> m b.

Answer 3

Algunos conceptos útiles para usar aquí:

1. Cualquier tipo con una variable a se puede convertir en un tipo diferente mediante la sustitución de cada instancia de a con cualquier otro tipo t. Por lo tanto, si tiene el tipo a -> b -> c, puede obtener el tipo a -> d -> c o el tipo a -> b -> Int reemplazando b con d o c con Int respectivamente.
2. Dos tipos que se pueden convertir el uno al otro por reemplazo son equivalentes. Por ejemplo, a -> b y c -> d son equivalentes (a ~ c, b ~ d).
3. Si un tipo t se puede convertir en un tipo t', pero t' no se puede convertir de nuevo a t, entonces se dice que es un t' especialización de t. Por ejemplo, a -> a es una especialización de a -> b.

Ahora, con estos conceptos muy útiles, la respuesta a su pregunta es muy simple: incluso si los tipos "nativos" de la función no coinciden exactamente, son compatibles porque pueden reescribirse o especializados para obtener esa coincidencia exacta. La respuesta de Matt Fenwick muestra las especializaciones que lo hacen para este caso.