CODEWITHSUNDEEP
haskelltypesfunctional-programming
JimmyP
JimmyP

Reputation: 444

How Do I Read This Hole Error

I am trying to write an implementation of flatMap. But this is inconsequential, I'm really interested in understanding the error message. But for context so far I have:

flatMap ::
(a -> List b)
  -> List a
  -> List b
flatMap f xs = foldRight undefined undefined _undefined

This gives the following error for the type hole:

Found hole ‘_undefined’ with type: List a0
    Where: ‘a0’ is an ambiguous type variable
    Relevant bindings include
      xs :: List a (bound at src/Course/List.hs:266:11)
      f :: a -> List b (bound at src/Course/List.hs:266:9)
      flatMap :: (a -> List b) -> List a -> List b
        (bound at src/Course/List.hs:266:1)
    In the third argument of ‘foldRight’, namely ‘_undefined’
    In the expression: foldRight undefined undefined _undefined
    In an equation for ‘flatMap’:
        flatMap f xs = foldRight undefined undefined _undefined

I know the right peg for this hole is xs, but I dont understand why the haskell compiler has given it a type denoted List a0 and how that relates to the type I'm going to use of List a?

I think it has something to do with the fact that the whole could take a superset of the type List a or something? by why then didn't it just call it List b instead of specifically List a0.

Cheers, Jim

Upvotes: 3

Views: 832

Answers (1)

chi
chi

Reputation: 116139

Roughly, the compiler infers types as follows.

Let's give to each undefined a distinct type unknown:

flatMap :: (a -> List b) -> List a -> List b
flatMap f xs =
   foldRight (undefined :: a1) (undefined :: b1) (_undefined :: c1)

Now, foldRight expects a binary function having a type like a2 -> b2 -> b2, so let's make a1 more precise.

flatMap :: (a -> List b) -> List a -> List b
flatMap f xs =
   foldRight (undefined :: a2 -> b2 -> b2) (undefined :: b1) (_undefined :: c1)

Now, foldRight requires that the second undefined has type b1 ~ b2, while the last one must have type c1 ~ List a2.

flatMap :: (a -> List b) -> List a -> List b
flatMap f xs =
   foldRight (undefined :: a2 -> b2 -> b2) (undefined :: b2) (_undefined :: List a2)

(assuming we have Nil and Cons as constructors of your List type)

The result of foldRight is b2, but the type signatures says this is actually List b. Hence,

flatMap :: (a -> List b) -> List a -> List b
flatMap f xs =
   foldRight (undefined :: a2 -> List b -> List b) (undefined :: List b)
             (_undefined :: List a2)

Now we are done. Note that there are no constraints which can allow us to deduce that a2 ~ a, so a2 remains an unknown, and the compiler cannot suggest a more precise type for it, and your hole generates the GHC message you posted.

More concretely, look at this specialization where a2 ~ Int:

flatMap :: (a -> List b) -> List a -> List b
flatMap f xs =
   foldRight (g :: Int -> List b -> List b) (Nil :: List b) (Cons 3 Nil :: List Int)
   where g :: Int -> List b -> List b
         g y ys = ys

The above type checks, even if we chose a2 ~ Int instead of a2 ~ a. Hence the compiler cannot infer a2 ~ a, since there are more solutions to the type unknown a2.

Upvotes: 4

Related Questions