¿Puedo imprimir en Haskell el tipo de función polimórfica como se convertiría si le pasara una entidad de un tipo concreto?

Dec 12 2020

Aquí hay una función polimórfica en 3 tipos:

:t (.)
(.) :: (b -> c) -> (a -> b) -> a -> c

y aquí una función no polimórfica:

:t Data.Char.digitToInt
Data.Char.digitToInt :: Char -> Int

Si aplicamos lo primero a lo segundo, obtenemos una función polimórfica en 1 tipo:

:t (.) Data.Char.digitToInt
(.) Data.Char.digitToInt :: (a -> Char) -> a -> Int

lo que significa que (.)fue "instanciado" (no estoy seguro de que este sea el término correcto; como programador de C ++, lo llamaría así) con b === Chary c === Int, por lo que la firma del (.)que se aplica digitToIntes la siguiente

(Char -> Int) -> (a -> Char) -> a -> Int

Mi pregunta es: ¿hay alguna manera de tener esta firma impresa en pantalla, dada (.), digitToInty la "información" que quiero aplicar la primera a la segunda?

Para quién esté interesado, esta pregunta se cerró anteriormente como duplicado de esta .

Respuestas

7 MikeSpivey Dec 13 2020 at 06:32

Otras respuestas requieren la ayuda de funciones que se han definido con tipos restringidos artificialmente, como la asTypeOffunción en la respuesta de HTNW. Esto no es necesario, como muestra la siguiente interacción:

Prelude> let asAppliedTo f x = const f (f x)

Prelude> :t head `asAppliedTo` "x"
head `asAppliedTo` "x" :: [Char] -> Char

Prelude> :t (.) `asAppliedTo` Data.Char.digitToInt
(.) `asAppliedTo` Data.Char.digitToInt
  :: (Char -> Int) -> (a -> Char) -> a -> Int

Esto aprovecha la falta de polimorfismo en el enlace lambda implícito en la definición de asAppliedTo. Ambas ocurrencias de fen su cuerpo deben recibir el mismo tipo, y ese es el tipo de su resultado. La función constutilizada aquí también tiene su tipo natural a -> b -> a:

const x y = x
12 HTNW Dec 12 2020 at 09:09

Hay esta pequeña función ordenada escondida en una esquina de Prelude:

Prelude.asTypeOf :: a -> a -> a
asTypeOf x _ = x

Está documentado como "forzar su primer argumento a tener el mismo tipo que el segundo". Podemos usar esto para forzar el (.)primer argumento del tipo de :

-- (.) = \x -> (.) x = \x -> (.) $ x `asTypeOf` Data.Char.digitToInt -- eta expansion followed by definition of asTypeOf -- the RHS is just (.), but restricted to arguments with the same type as digitToInt -- "what is the type of (.) when the first argument is (of the same type as) digitToInt?" ghci> :t \x -> (.) $ x `asTypeOf` Data.Char.digitToInt
\x -> (.) $ x `asTypeOf` Data.Char.digitToInt
  :: (Char -> Int) -> (a -> Char) -> a -> Int

Por supuesto, esto funciona para tantos argumentos como necesite.

ghci> :t \x y -> (x `asTypeOf` Data.Char.digitToInt) . (y `asTypeOf` head)
\x y -> (x `asTypeOf` Data.Char.digitToInt) . (y `asTypeOf` head)
  :: (Char -> Int) -> ([Char] -> Char) -> [Char] -> Int

Puede considerar esto como una variación de la idea de @ KABuhr en los comentarios, usando una función con una firma más restrictiva que su implementación para guiar la inferencia de tipos, excepto que no tenemos que definir nada nosotros mismos, a costa de no poder simplemente Copie la expresión en cuestión debajo de una lambda.

8 K.A.Buhr Dec 12 2020 at 09:57

Creo que la respuesta de @ HTNW probablemente lo cubre, pero para completar, así es como funciona la inContextsolución en detalle.

La firma de tipo de la función:

inContext :: a -> (a -> b) -> a

significa que, si tiene algo que desea escribir y un "contexto" en el que se usa (expresable como una lambda que lo toma como argumento), digamos con tipos:

thing :: a1
context :: a2 -> b

Puede forzar la unificación de a1(el tipo general de thing) con a2(las restricciones del contexto) simplemente construyendo la expresión:

thing `inContext` context

Normalmente, el tipo unificado thing :: ase perdería, pero la firma de tipo de inContextimplica que el tipo de toda esta expresión resultante también se unificará con el tipo deseado a, y GHCi felizmente le dirá el tipo de esa expresión.

Entonces la expresión:

(.) `inContext` \hole -> hole digitToInt

termina obteniendo asignado el tipo que (.)tendría dentro del contexto especificado. Puede escribir esto, de manera algo engañosa, como:

(.) `inContext` \(.) -> (.) digitToInt

ya que (.)es un nombre de argumento tan bueno como es para una lambda anónima hole. Esto es potencialmente confuso, ya que estamos creando un enlace local que sombrea la definición de nivel superior de (.), pero sigue nombrando lo mismo (con un tipo refinado), y este abuso de lambdas nos permitió escribir la expresión original (.) digitToIntpalabra por palabra, con la placa de calderas adecuada.

En realidad, es irrelevante cómo inContextse define, si solo le pregunta a GHCi por su tipo, inContext = undefinedhabría funcionado. Pero, con solo mirar la firma de tipo, es bastante fácil dar inContextuna definición de trabajo:

inContext :: a -> (a -> b) -> a
inContext a _ = a

Resulta que esta es solo la definición de const, por lo que también inContext = constfunciona.

Puede usar inContextpara escribir varias cosas a la vez, y pueden ser expresiones en lugar de nombres. Para acomodar el primero, puede usar tuplas; para que esto último funcione, debe usar nombres de argumentos más sensibles en sus lambas.

Así por ejemplo:

λ> :t (fromJust, fmap length) `inContext` \(a,b) -> a . b
(fromJust, fmap length) `inContext` \(a,b) -> a . b
  :: Foldable t => (Maybe Int -> Int, Maybe (t a) -> Maybe Int)

te dice que en la expresión fromJust . fmap length, los tipos se han especializado en:

fromJust :: Maybe Int -> Int
fmap length :: Foldable t => Maybe (t a) -> Maybe Int
6 FyodorSoikin Dec 12 2020 at 03:35

Puede hacerlo usando la TypeApplicationsextensión, que le permite especificar explícitamente qué tipos desea usar para crear una instancia de los parámetros de tipo:

λ :set -XTypeApplications                                 
λ :t (.) @Char @Int
(.) @Char @Int :: (Char -> Int) -> (a -> Char) -> a -> Int

Tenga en cuenta que los argumentos deben estar en el orden exacto.

Para las funciones que tienen una firma de tipo "regular" como foo :: a -> b, el orden se define por el orden en el que los parámetros de tipo aparecen por primera vez en la firma.

Para las funciones que usan ExplicitForalllike foo :: forall b a. a -> b, el orden está definido por lo que sea forall.


Si desea averiguar el tipo basado específicamente en la aplicación (.)de digitToChar(en comparación con el hecho de saber qué tipos de relleno), estoy bastante seguro de que puede no en GHCi, pero que recomiendo encarecidamente el apoyo Haskell IDE.

Por ejemplo, así es como me ve en VSCode (aquí está la extensión ):

5 chi Dec 12 2020 at 16:39

Esta es una variación menor de la respuesta de HTNW.

Supongamos que tenemos cualquier expresión potencialmente grande que involucre un identificador polimórfico poly

 .... poly ....

y nos preguntamos cómo se instancia el tipo polimórfico en ese punto.

Esto se puede hacer aprovechando dos características de GHC: asTypeOf(como lo menciona HTNW) y agujeros escritos , de la siguiente manera:

 .... (poly `asTypeOf` _) ....

Al leer el _hoyo, GHC generará un error informando el tipo de término que se debe ingresar en lugar de ese hoyo. Dado que usamos asTypeOf, esto debe ser el mismo que el tipo de instancia particular de polyque necesitamos en ese contexto.

Aquí hay un ejemplo en GHCi:

> ((.) `asTypeOf` _) Data.Char.digitToInt
<interactive>:11:17: error:
    * Found hole: _ :: (Char -> Int) -> (a -> Char) -> a -> Int