Disappearing applicative?

Question

I'm a bit confused about the behavior of pure in a case where its Applicative instance is unspecified. In this example, I expect the resulting value to be the number 5 in an applicative context:

Prelude> pure 5 :: Applicative t => t Integer
5
Prelude> :t it
it :: Integer

Instead, it's just a plain Integer.

If the applicative instance is specified, like in the following example, the returned value is in an applicative type, as I expect:

Prelude> pure 5 :: Maybe Integer
Just 5
Prelude> :t it
it :: Maybe Integer

Why does the Applicative t seem to disappear in the first example?

It seems that the unspecified applicative context is being stripped off for the final evaluation to print to the output, but I'd like to know what the rules are for this.

I could be wrong, but I think GHCi defaults `t` to be `IO`, and `it` is bound to the result of executing the resulting action. — chepner, Apr 05 '22 at 00:16
This is a result of having to find a specific type in order to evaluate and show the resulting expression; `x = pure 5 :: Applicative t => t Integer` preserves the polymorphic type of `x`. — chepner, Apr 05 '22 at 00:17

score 6 · Accepted Answer · answered Apr 05 '22 at 00:26

This is a GHCi peculiarity briefly discussed here. When an expression is entered at the GHCi prompt and evaluated, if its type can be unified with IO a, then it will be executed as an IO action with return type a, and the return value of the action will be displayed (if it is other than () and if it has a Show instance).

It turns out that the corresponding value of it will be set to the return value of the IO action, rather than the IO action itself. I guess the idea is that, if you were to write:

> getLine
I typed this!    <-- what I typed
"I typed this!"  <-- the return value displayed

you'd want it to give the returned value, not re-run the IO action:

> it
"I typed this!"
> :t it
it :: String

Specifically, in your case, the type of the expression:

> pure 5 :: Applicative t => t Integer

can be unified with IO Integer, and so it is. The IO action is run, the return value is 5, and that becomes both the output and the value of it.

Note what happens if you write an expression that can't be unified with IO:

> pure 5 :: (Applicative t, Foldable t) => t Integer
[5]

Here, because IO has no Foldable instance in scope, the type can't unify with IO, and instead GHCi's "extended defaulting" rules for assigning types to unspecified type variables are used. These extended rules include using the list type [] for unknown types of kind * -> *, so we get pure 5 :: [Integer]. If we first add a Foldable IO instance, then unification with IO works again, and we get the behavior you already observed:

> instance Foldable IO   -- this works, despite the warning

<interactive>:11:10: warning: [-Wmissing-methods]
    • No explicit implementation for
        either ‘foldMap’ or ‘foldr’
    • In the instance declaration for ‘Foldable IO’
> pure 5 :: (Applicative m, Foldable m) => m Integer
5

Disappearing applicative?

1 Answers1