Resolving the type of `f = f (<*>) pure`

Question

Recently I noticed that humourously liftA can be written as

liftA (<*>) pure

I thought this was neat and so as a bit of a joke I thought I would make a new "definition" of liftA based on this property:

f = f (<*>) pure

Now I had expected that this would be something of the same type as liftA that just never halted. However it fails to compile.

• Occurs check: cannot construct the infinite type:
    t ~ (f (a -> b) -> f a -> f b) -> (a1 -> f1 a1) -> t
• In the expression: f (<*>) pure
  In an equation for ‘f’: f = f (<*>) pure
• Relevant bindings include
    f :: (f (a -> b) -> f a -> f b) -> (a1 -> f1 a1) -> t
      (bound at liftA.hs:2:1)

This seems sensible, I see how the compiler has an issue. However things get a little weird because when I add an annotation:

f :: Applicative f => (a -> b) -> f a -> f b
f = f (<*>) pure

It suddenly compiles.

Now my initial suspicion was that the type I was annotating f with was not the most general type and that by restricting the type I had made it possible to unify things. However looking at the types this doesn't seem to be the case my type seems to be more general than the type that the compiler was trying to derive.

What is going on here? I am a bit out of my depth here but I am curious as to what the compiler is thinking in each scenario and why it encounters an issue in one but not the other.

Answer 1

The confusion is caused by Haskell's type classes and the fact that functions-from-fixed-type are an instance of Applicative (aka the reader monad). It becomes clearer if you write it out with specialised version:

type Reader a b = a -> b

fmapFn :: (a -> b) -> Reader c a -> Reader c b
fmapFn = fmap
    -- ≡ liftA
    -- ≡ (.)

fmap' :: Applicative f => (a -> b) -> f a -> f b
fmap' = fmapFn (<*>) pure
      ≡ (<*>) . pure
      ≡ \φ -> (<*>) (pure φ)
      ≡ \φ fa -> pure φ <*> fa

And at this point it requires the applicative law

fmap f x = pure f <*> x

so

 fmap' ≡ \φ fa -> fmap φ fa
       ≡ fmap

duh. But the point is, in the definition fmap' = fmap' (<*>) pure, the (<*>) and pure belong to the functor for which you want this to eventually work, but the fmap' you're using actually always belongs to the function functor. That's ok in Haskell: the definition is polymorphic after all, so if the top-level knows how to do this for all functors then you can certainly also use it for the function functor. (Leaving aside the issue of nontermination due to circular dependency...) However, because you're defining it in the form fmap' = ..., the monomorphism restriction kicks in: if you write fmap' = fmap' (<*>) pure without signature at the top-level, the compiler tries to find a concrete type for which this should work, in particular a single, concrete functor. But whatever concrete type you choose, this will then be a different type from the fmapFn that you're trying to use yourself. So, this definition only compiles with an explicit signature that forces it to be polymorphic (or alternatively, with the -XNoMonomorphismRestriction flag, which causes the compiler to pick the polymorphic type without explicit instruction).

^EDIT Surprisingly it turns out it is not the monomorphism restriction what tries to make the type less polymorphic than necessary. To figure out what it is, let's try to find a simpler example with the same problem. First attempt:

fromFloat :: RealFrac a => Float -> a
toFloat :: RealFrac a => a -> Float
fromFloat = realToFrac
toFloat   = realToFrac

s = fromFloat . s . toFloat

(I chose Float because it's not a default type that the compiler might pick by itself.)
Turns out this compiles just fine, but instead of the most general type

s' :: (RealFrac a, RealFrac b) => a -> b
s' = fromFloat . s' . toFloat

it just picks up the simpler

s :: Float -> Float

...regardless of whether the monomorphism restriction is enabled. Why? I don't know; I'd find this an interesting question to ask.

Answer 2

It’s because the f used in the body of the definition of f has a different type than the definition. This is called polymorphic recursion, and Haskell only allows that if you provide a type signature. The reason for requiring a type signature is that type inference for polymorphic recursion is undecidable in the general case.