How does polymorphic recursion relate to infinite type errors?

Question

Context: I ran into a problem and got help here, however I realized I don't understand the solution.

The keyword appears to be polymorphic recursion. I thought that foldr is polymorphic and recursive, but this seems to be a different concept.

This explicit recursion works (based on shell-monad):

cmdList :: (Param command, Param arg, CmdParams result) =>
    command -> [arg] -> result
cmdList command = go . reverse where
    go :: (Param arg, CmdParams result) => [arg] -> result
    go [] = cmd command
    go (arg:args) = go args arg

But trying to refactor the answer towards my original attempts using foldr I quickly ran into the problem I struggled with initially: infinite types. Replacing a constant cmd command with b:

go :: (Param arg, CmdParams result) => result -> [arg] -> result
go b [] = b
go b (arg:args) = go b args arg

    • Occurs check: cannot construct the infinite type:
        result ~ arg -> result
    • In the expression: go b args arg

It seems to me that GHC no longer accepts polymorphic result that is either a value or a function.

1. Why does that happen?

2. Can I not use foldr in such cases?

Answer 1

Here's a simple recursive function:

ignore :: [a] -> ()
ignore [] = ()
ignore (a:as) = ignore as

It is polymorphic, and it is recursive. But, like almost all recursions, whatever type the caller chooses for a, the recursion happens using the same choice for a. That is, we could write this, with ScopedTypeVariables and probably a handful of other extensions:

ignore :: forall a. [a] -> ()
ignore (a:as) = ignore @a as

The term "polymorphic recursion" refers to a very special kind of recursion, where the recursive call chooses a different type for some parameter. The standard example is this one:

data BalancedTree a = Leaf a | Branch (BalancedTree (a, a))

foldBT :: (a -> a -> a) -> BalancedTree a -> a
foldBT f (Leaf a) = a
foldBT f (Branch bt) = uncurry f $ foldBT (\(x, y) (x', y') -> (f x x', f y y')) bt

(For example, foldBT (+) would add all the elements of the tree.)

The special thing here is that the recursive call to foldBT is not recursing over a BalancedTree a -- but over a BalancedTree (a, a) instead. The type has changed, like this:

foldBT :: forall a. (a -> a -> a) -> BalancedTree a -> a
foldBT f (Branch bt) = uncurry f $ foldBT @(a, a) {- N.B. not a! -} (\(x, y) (x', y') -> (f x x', f y y')) bt

It turns out that type inference in the setting that allows this kind of thing is pretty hard. To deal with that, Haskell has a restriction: inferred types always use monomorphic recursion, that is, all recursive calls choose all the same values for the type variables involved. You can still get polymorphic recursion by giving an appropriate type signature, because then inference is not needed.

Now, in your working situation, you write

cmdList :: forall command arg result.
    (Param command, Param arg, CmdParams result) =>
    command -> [arg] -> result
cmdList command = go . reverse where
    -- for clarity, I have chosen fresh type variable names
    go :: forall arg' result'. (Param arg', CmdParams result') => [arg'] -> result'
    go [] = cmd command
    go (arg:args) = go args arg

Notice that in the recursive case, go is being given an extra argument on the right hand side of the equation compared to the left! This is polymorphic recursion; the result type is slowly accumulating extra arguments.

go (arg:args) = go @arg' @(arg' -> result') {- N.B. not result'! -} args arg

This means that in the base case,

go [] = cmd command

the type of cmd may be different depending on how many arguments there are in the list! In other words, you can think of events happening in this order: first the user chooses a command type, an argument type, and a result type; then you traverse the list and choose a different result type that accepts more arguments; then you call cmd with that newly chosen result type.

Compare the version that doesn't work:

go :: (Param arg, CmdParams result) => result -> [arg] -> result
go b [] = b
go b (arg:args) = go b args arg

In this version, a choice has been lost; first the user chooses a result type, then you traverse the list and choose the same result type as the user did; then you use their b of that type. But this is a problem -- they may not have chosen the right number of arguments for that list, and even if they did, it's not really reasonable to expect the compiler to be able to know that statically!

This explains the occurs check error you've gotten: for go to work right in this setting, its b argument has to be able to accept an arbitrary number of arguments, and there just isn't any single type that does that.

It also explains why you cannot use foldr: foldr is implemented with monomorphic recursion. It is probably possible to create a variant of foldr using RankNTypes that could sit in this spot, but I suspect it's more work than it's worth.

And, by the way, I think you can make your refactoring work, though I'm not 100% because I haven't installed shell-monad to check this. But it would look something like this:

go :: (Param arg, CmdParams result) => (forall result'. CmdParams result') -> [arg] -> result
-- same implementation as before

The key here is that putting the extra forall there forces the first b argument to be polymorphic; this lets you choose result' to be a suitably-many-arguments variant of result when you get to the base case.