Herramienta o método de resolución de parámetros de tipo genérico Haskell [duplicado]

Dec 12 2020

Veamos los tipos de estas funciones, por ejemplo:

:t traverse
traverse
  :: (Applicative f, Traversable t) => (a -> f b) -> t a -> f (t b)

:t id
id :: a -> a

No tienen tipos de hormigón, pero tienen parámetros de tipo genérico : a, f, b, t(corríjanme si no que llamaron parámetros de tipo genérico , por favor)

Si combino idy traversejunto de esta manera,

:t traverse id [Just 1, Just 2, Nothing] 
traverse id [Just 1, Just 2, Nothing] :: Num b => Maybe [b]

Haskell ahora se puede unir algunos tipos concretos de las variables de tipo a, f, b, t.

t = []
a = Maybe bb
f = Maybe
b = Num bb => bb

A continuación, infiero los tipos y asignaciones a los parámetros a mano, ¿hay alguna forma o herramienta en Haskell para hacer esto automáticamente, de modo que tome algunas partes compuestas ( idy traverse) en un ejemplo, extraiga sus firmas de tipo en general, y en la salida produzca ¿un mapeo de nombres de parámetros de tipo genérico a tipos inferidos concretos?

Vea también el primer ejemplo aquí: https://wiki.haskell.org/Type_inferencepara la expresión " map ord" sobre cómo Haskell encuentra enlaces de tipos reales a nombres.

Así que cuando nos fijamos en funciones por separado sólo tenemos nombres a, f, b, t. Pero entonces nos combinamos las funciones y proporcionar alguna información extra, como [Just 1, Just 2, Nothing], y los nombres a, f, b, tse asignan a tipos concretos.

Quiero capturar y mostrar este mapeo automáticamente.

Respuestas

Enlico Dec 12 2020 at 00:55

Creo que fy tson parámetros de constructor de tipos más genéricos , ya que actúan sobre un tipo para darte un tipo ( tipo es * -> *, donde *significa "un tipo concreto").

traverse idNo es la composición, es la aplicación de funciones, ya que está de paso idcomo un argumento a traverse. this . thates la composición de funciones entre thisy that, en el sentido matemático, donde se crea una función que proporciona su (primer) argumento como entrada thaty alimenta el resultado de esta aplicación a this.

Consulte el ejemplo de esta página, donde se proporciona este

map :: (a -> b) -> [a] -> [b]
Char.ord :: (Char -> Int)

el compilador puede deducir que el tipo de map ordes [Char] -> [Int], ya que puede comprobarlo escribiendo :t map orden la línea de comandos.

Si espera una salida similar con tipos concretos cuando escribe :t traverse id, no la obtendrá, por la sencilla razón de que traverse idsigue siendo una función polimórfica, tanto en sus argumentos de tipo concreto como en sus argumentos de constructor de tipo.

Solo para dar un ejemplo ligeramente diferente, si escribe :t traverse (:[]), where (:[])has type a -> [a], que es un caso particular del (Applicative f) => a -> f bque traverseespera, obtiene este resultado,

traverse (:[]) :: Traversable t => t b -> [t b]

que, en comparación con :t traverse,

traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)

le dice que traverse, en traverse (:[]), se ha "instanciado" con f === []y a === b.