7
votes

If I have this insert function:

insert x []     = [x]
insert x (h:t)
  | x <= h      = x:(h:t)
  | otherwise   = h:(insert x t)

this produces a sorted list:

foldr insert [] [1,19,-2,7,43]

but this:

foldr1 insert [1,19,-2,7,43]

produces 'cannot construct the infinite type: a0 = [a0]'

I'm confused about why the second call cannot work.

I have looked at the definitions for both foldr and foldr1 and have traced both with simple arithmetic functions, but I still cannot come up with a clear explanation for why the second call fails.

5

5 Answers

16
votes

Let's look at some type signatures.

foldr  :: (a -> b -> b) -> b -> [a] -> b
foldr1 :: (a -> a -> a) ->      [a] -> a

In both cases, the first argument is a function of two arguments.

  • for foldr1, these two arguments must have the same type (and the result has this type also)
  • for foldr, these two arguments may have different types (and the result has the same type as the second argument)

What's the type of your insert?

11
votes

I like the type-based answers given here, but I also want to give an operational one explaining why we don't want this to typecheck. Let's take the source of foldr1 to start with:

foldr1          :: (a -> a -> a) -> [a] -> a
foldr1 _ [x]    = x
foldr1 f (x:xs) = f x (foldr1 f xs)

Now, let's try running your program.

foldr1 insert [1,19,-2,7,43]
= { list syntax }
foldr1 insert (1:[19,-2,7,43])
= { definition of foldr1 }
insert 1 (foldr1 insert [19,-2,7,43])
= { three copies of the above two steps }
insert 1 (insert 19 (insert (-2) (insert 7 (foldr1 insert [43]))))
= { definition of foldr1 }
insert 1 (insert 19 (insert (-2) (insert 7 43)))

...whoops! That insert 7 43 is never going to work. =)

4
votes

The type of foldr1 is (a -> a -> a) -> [a] -> a, i.e. arguments and result of this function have the same type. However, insert has type Ord a => a -> [a] -> [a]. For foldr1 insert being well-typed, a and [a] must be the same type.

But this would mean that a == [a] == [[a]] == [[[a]]] == ..., i.e., a being a type of infinitely many lists.

1
votes

Because foldr1 is trying to do this:

insert 43 -7

which will fail.

1
votes

The problem is following:

foldr would do this way:

  1. result set to insert 43 []
  2. result set to insert 7 result
  3. and so on

This clearly works.

Whereas foldr1 would try to do the following:

  1. result set to insert 7 43
  2. result set to insert -2 result
  3. etc.

which is definitely wrong. You can see, foldr1 requires the arguments to the operation to be of the same type, which is not the case for insert.