Can I print in Haskell the type of a polymorphic function as it would become if I passed to it an entity of a concrete type?

Question

Here's a function polymorphic in 3 types:

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

and here a non polymorphic function:

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

If we apply the former to the latter, we get a function polymorphic in 1 type:

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

which means that (.) was "instantiated" (I'm not sure this is the correct term; as a C++ programmer, I'd call it so) with b === Char and c === Int, so the signature of the (.) that gets applied to digitToInt is the following

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

My question is: is there a way to have this signature printed on screen, given (.), digitToInt and the "information" that I want to apply the former to the latter?

For who's interested, this question was earlier closed as duplicate of this one.

Wundt

in what language? this answer of mine contains a Prolog snippet that does that. – Torsi

@WillNess, I was thinking about doing it from within ghci. – Wundt

what's wrong with > :t (.) Data.Char.digitToInt? – Torsi

@WillNess, that is not telling me what the type of the first argument to (.) is. Yes, I know, it's the type of the argument I'm giving to it, but that's the point of my question. – Wundt

Check out my answer at the linked duplicate. For your exact question, the instantiation of the principle described there would be :t undefined :: ((b -> c) -> (a -> b) -> a -> c) ~ ((Char -> Int) -> d) => ((b -> c) -> (a -> b) -> a -> c), which replies ... :: (Char -> Int) -> (a -> Char) -> a -> Int. – Jayjaycee

@Wundt Hm. Maybe? I'm not sure what "part of signature" and "rest of signature" mean to you. For function application specifically, the pattern is :t undefined :: (type of function) ~ (type of argument -> fresh variable) => (comma separated unknowns) (where the unknown could be, say, another copy of the function's type signature). If both the function and the argument are polymorphic, you should make sure to rename the variables in one or the other so there are no accidental equalities. – Jayjaycee

When working with concrete terms, it might be easier to define a helper inContext :: a -> (a -> b) -> a defined by inContext = const. Then, at the GHCi prompt, the expression inContext (.) $ \(.) -> (.) digitToInt gives the inferred type directly, so you don't have to copy type signatures and make up fresh variables. Note that inContext can be used infix, but I always mess up writing code with backticks in comments. – Ocasio

@K.A.Buhr code snippets in comments can be enclosed in double backticks, ``...``, so the backticks inside the code are handled properly: > :t (.) `inContext` \(.) -> (.) Data.Char.digitToInt. – Torsi

@K.A.Buhr your answer is excellent and should really be added as such somewhere, if not here. I'm voting to reopen just in case you want to post it here rather than at the duplicate, since it's not an exact duplicate anyway. – Torsi

Here’s a neat hack: you can ask for the type of an expression with the subexpression you care about annotated with a scoped type variable. This type variable will fail to unify with any concrete type, and in order to check that, the typechecker must instantiate the inferred type, and will thus report that instantiated type: :t let x :: forall t. _; x = ((.) :: t) digitToInt in x says it can’t match t with (Char -> Int) -> (a -> Char) -> a -> Int. You can save this in your .ghci file as a custom command like :def itype \ expr -> …, but I think it’d be better to make a feature request. – Shaquana

@DanielWagner I've voted to reopen since there are more answers being shown in the comments here which probably ought to be posted as such, and I'm not sure where their authors would prefer to post them. – Torsi

Okay, sure. Though it's a bit of a shame that this question page no longer has a way for future readers to discover the link to the other question (e.g. it doesn't appear in the "Linked" list on the right), which I think you can agree is very closely related even if you don't think its answers apply here. – Jayjaycee

@DanielWagner, I have inscluded the link in the question now. – Wundt

@JonPurdy, I have to :set some extension for that, right? Would you explain that in an answer? I guess it could be useful for other readers. – Wundt

@DanielWagner the answers there do apply, but not directly, they must be tweaked a bit... as for the link being gone, there is a way to see the revisions even when there are none yet, by entering the URL manually (which I've included in my comment to you). you'd still see the link to the dup there even before the last edit on the question. :) (and now of course it has the clickable revisions link under it, titled "edited <time ago>", which contains the link to the dup). – Torsi

Answer 1

Other answers require the help of functions that have been defined with artificially restricted types, such as the asTypeOf function in the answer from HTNW. This is not necessary, as the following interaction shows:

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

This exploits the lack of polymorphism in the lambda-binding that is implicit in the definition of asAppliedTo. Both occurrences of f in its body must be given the same type, and that is the type of its result. The function const used here also has its natural type a -> b -> a:

const x y = x

Malone

Answer 2

There's this neat little function hidden in a corner of the Prelude:

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

It's documented as "forcing its first argument to have the same type as the second." We can use this to force the type of (.)'s first argument:

-- (.) = \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

Of course, this works for as many arguments as you need.

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

You can consider this a variation of @K.A.Buhr's idea in the comments—using a function with a signature more restrictive than its implementation to guide type inference—except we don't have to define anything ourselves, at the cost of not being able to just copy the expression in question under a lambda.

Translucent

Indeed, my discovery of asTypeOf many years ago inspired my solution. – Ocasio

Answer 3

I think @HTNW's answer probably covers it, but for completeness, here's how the inContext solution works in detail.

The type signature of the function:

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

means that, if you have a thing you want to type, and a "context" in which it's used (expressible as a lambda that takes it as an argument), say with types:

thing :: a1
context :: a2 -> b

You can force unification of a1 (the general type of thing) with a2 (the constraints of the context) simply by constructing the expression:

thing `inContext` context

Normally, the unified type thing :: a would be lost, but the type signature of inContext implies that the type of this whole resulting expression will also be unified with the desired type a, and GHCi will happily tell you the type of that expression.

So the expression:

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

ends up getting assigned the type that (.) would have within the specified context. You can write this, somewhat misleadingly, as:

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

since (.) is as good an argument name for an anonymous lambda as hole is. This is potentially confusing, since we're creating a local binding that shadows the top-level definition of (.), but it's still naming the same thing (with a refined type), and this abuse of lambdas allowed us to write the original expression (.) digitToInt verbatim, with the appropriate boilerplate.

It's actually irrelevant how inContext is defined, if you're just asking GHCi for its type, so inContext = undefined would have worked. But, just looking at the type signature, it's easy enough to give inContext a working definition:

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

It turns out that this is just the definition of const, so inContext = const works, too.

You can use inContext to type multiple things at once, and they can be expressions instead of names. To accommodate the former, you can use tuples; for the latter to work, you have use more sensible argument names in your lambas.

So, for example:

λ> :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)

tells you that in the expression fromJust . fmap length, the types have been specialized to:

fromJust :: Maybe Int -> Int
fmap length :: Foldable t => Maybe (t a) -> Maybe Int

Ocasio

Answer 4

You can do that using the TypeApplications extension, which allow you to explicitly specify which types you want to use to instantiate type parameters:

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

Note that the arguments must be in the exact order.

For functions that have a "regular" type signature like foo :: a -> b, the order is defined by the order in which the type parameters first appear in the signature.

For functions that use ExplicitForall like foo :: forall b a. a -> b, the order is defined by whatever it is in forall.

---

If you want to figure out the type specifically based on applying (.) to digitToChar (as opposed to just knowing which types to fill), I'm pretty sure you can't in GHCi, but I can highly recommend Haskell IDE support.

For example, here's how it looks for me in VSCode (here's the extension):

Dikdik

Looks like it just replaces the placeholders with specific types. The question asks: is there a way to type something like :t (.) Data.Char.digitToInt instead of :t (.) @Int @Char? – Decompensation

Answer 5

This is a minor variation on HTNW's answer.

Suppose we have any, potentially large, expression involving a polymorphic identifier poly

 .... poly ....

and we wonder how the polymorphic type was instantiated at that point.

This can be done exploiting two features of GHC: asTypeOf (as mentioned by HTNW) and typed holes, as follows:

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

Upon reading the _ hole, GHC will generate an error reporting the type of the term that should be entered in place of that hole. Since we used asTypeOf, this must be the same as the type of the particular instance of poly we need in that context.

Here's an example in GHCi:

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

Anatomy