Puis-je imprimer en Haskell le type d'une fonction polymorphe telle qu'elle deviendrait si je lui passais une entité de type concret?
Voici une fonction polymorphe en 3 types:
:t (.)
(.) :: (b -> c) -> (a -> b) -> a -> c
et ici une fonction non polymorphe:
:t Data.Char.digitToInt
Data.Char.digitToInt :: Char -> Int
Si on applique le premier au second, on obtient une fonction polymorphe en 1 type:
:t (.) Data.Char.digitToInt
(.) Data.Char.digitToInt :: (a -> Char) -> a -> Int
ce qui signifie que cela a (.)été "instancié" (je ne suis pas sûr que ce soit le terme correct; en tant que programmeur C ++, je l'appellerais ainsi) avec b === Charet c === Int, donc la signature du (.)qui est appliqué digitToIntest la suivante
(Char -> Int) -> (a -> Char) -> a -> Int
Ma question est: y a-t-il un moyen d'avoir cette signature imprimée à l'écran, donnée (.), digitToIntet les "informations" que je veux appliquer la première à la seconde?
Pour qui est intéressé, cette question a été fermée plus tôt en double de celle-ci .
Réponses
D'autres réponses nécessitent l'aide de fonctions qui ont été définies avec des types artificiellement restreints, comme la asTypeOffonction dans la réponse de HTNW. Cela n'est pas nécessaire, comme le montre l'interaction suivante:
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
Cela exploite le manque de polymorphisme dans la liaison lambda qui est implicite dans la définition de asAppliedTo. Les deux occurrences de fdans son corps doivent avoir le même type, et c'est le type de son résultat. La fonction constutilisée ici a également son type naturel a -> b -> a:
const x y = x
Il y a cette jolie petite fonction cachée dans un coin du Prelude:
Prelude.asTypeOf :: a -> a -> a
asTypeOf x _ = x
Il est documenté comme «forçant son premier argument à avoir le même type que le second». Nous pouvons utiliser ceci pour forcer le (.)premier argument du type 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
Bien sûr, cela fonctionne pour autant d'arguments que nécessaire.
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
Vous pouvez considérer cela comme une variante de l'idée de @ KABuhr dans les commentaires - en utilisant une fonction avec une signature plus restrictive que son implémentation pour guider l'inférence de type - sauf que nous n'avons rien à définir nous-mêmes, au prix de ne pas pouvoir simplement copiez l'expression en question sous un lambda.
Je pense que la réponse de @ HTNW le couvre probablement, mais pour être complet, voici comment la inContextsolution fonctionne en détail.
La signature de type de la fonction:
inContext :: a -> (a -> b) -> a
signifie que, si vous avez un élément que vous voulez taper, et un "contexte" dans lequel il est utilisé (exprimable comme un lambda qui le prend comme argument), dites avec les types:
thing :: a1
context :: a2 -> b
Vous pouvez forcer l'unification de a1(le type général de thing) avec a2(les contraintes du contexte) simplement en construisant l'expression:
thing `inContext` context
Normalement, le type unifié thing :: aserait perdu, mais la signature de type de inContextimplique que le type de toute l'expression résultante sera également unifié avec le type souhaité a, et GHCi se fera un plaisir de vous indiquer le type de cette expression.
Donc l'expression:
(.) `inContext` \hole -> hole digitToInt
finit par se voir attribuer le type qui (.)aurait dans le contexte spécifié. Vous pouvez écrire ceci, de manière quelque peu trompeuse, comme suit:
(.) `inContext` \(.) -> (.) digitToInt
car (.)est aussi bon qu'un nom d'argument pour un lambda anonyme hole. Ceci est potentiellement déroutant, car nous créons une liaison locale qui occulte la définition de niveau supérieur de (.), mais elle nomme toujours la même chose (avec un type raffiné), et cet abus de lambdas nous a permis d'écrire (.) digitToIntmot à mot l' expression originale , avec le passe-partout approprié.
La façon dont inContextest définie n'a pas d'importance , si vous demandez simplement à GHCi son type, cela inContext = undefinedaurait fonctionné. Mais, en regardant simplement la signature de type, il est assez facile de donner inContextune définition fonctionnelle:
inContext :: a -> (a -> b) -> a
inContext a _ = a
Il s'avère que ce n'est que la définition de const, donc ça inContext = constmarche aussi.
Vous pouvez utiliser inContextpour taper plusieurs choses à la fois, et il peut s'agir d'expressions au lieu de noms. Pour accueillir le premier, vous pouvez utiliser des tuples; pour que ce dernier fonctionne, vous avez utilisé des noms d'arguments plus sensés dans vos lambas.
Ainsi, par exemple:
λ> :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)
vous indique que dans l'expression fromJust . fmap length, les types ont été spécialisés pour:
fromJust :: Maybe Int -> Int
fmap length :: Foldable t => Maybe (t a) -> Maybe Int
Vous pouvez le faire en utilisant l' TypeApplicationsextension, qui vous permet de spécifier explicitement les types que vous souhaitez utiliser pour instancier les paramètres de type:
λ :set -XTypeApplications
λ :t (.) @Char @Int
(.) @Char @Int :: (Char -> Int) -> (a -> Char) -> a -> Int
Notez que les arguments doivent être dans l'ordre exact.
Pour les fonctions qui ont une signature de type "régulière" comme foo :: a -> b, l'ordre est défini par l'ordre dans lequel les paramètres de type apparaissent pour la première fois dans la signature.
Pour les fonctions qui utilisent ExplicitForalllike foo :: forall b a. a -> b, l'ordre est défini par ce qu'il contient forall.
Si vous voulez déterminer le type spécifique basé sur l' application (.)à digitToChar(par opposition à juste savoir quels types de remplissage), je suis sûr que vous ne pouvez pas en GHCi, mais je vous recommande vivement le soutien Haskell IDE.
Par exemple, voici à quoi cela ressemble dans VSCode (voici l'extension ):
Il s'agit d'une variation mineure de la réponse de HTNW.
Supposons que nous ayons une expression potentiellement volumineuse impliquant un identifiant polymorphe poly
.... poly ....
et nous nous demandons comment le type polymorphe a été instancié à ce stade.
Cela peut être fait en exploitant deux fonctionnalités de GHC: asTypeOf(comme mentionné par HTNW) et des trous typés , comme suit:
.... (poly `asTypeOf` _) ....
Lors de la lecture du _trou, GHC générera une erreur signalant le type du terme qui devrait être entré à la place de ce trou. Depuis que nous l'avons utilisé asTypeOf, cela doit être le même que le type de l'instance particulière dont polynous avons besoin dans ce contexte.
Voici un exemple dans GHCi:
> ((.) `asTypeOf` _) Data.Char.digitToInt
<interactive>:11:17: error:
* Found hole: _ :: (Char -> Int) -> (a -> Char) -> a -> Int