haskellrecursionlambda-calculuschurch-encodingscott-encoding

Is there any non-recursive term that folds over a scott-encoded list?

Suppose that I have a scott-encoded list such as:

scott = (\ c n -> c 1 (\ c n -> c 2 (\ c n -> c 3 (\ c n -> n))))

I want a function that receives such kind of list and converts it to an actual list ([1,2,3]), except that such function can not be recursive. That is, it must be in eta-beta normal form. Does that function exist?

Solution

  • OK, I give it a shot. Feel free to correct me, because I'm not an expert on this.

    For arbitrary x and xs, it must be the case that toList (\c n -> c x xs) reduces to a term that is convertible to x : toList xs.

    This is only possible if we reduce the left hand side to c x xs by applying (\c n -> c x xs) to some c and n. So toList ~ (\f -> f ? ?). (BTW, this is the part where I couldn't think of a nice rigorous argument; I had some ideas but none very nice. I'd be happy to hear tips).

    Now it must be the case that c x xs ~ (x : toList xs). But since x and xs are distinct universal variables, and they are the only variables occurring in the right hand side, the equation is in Miller's pattern fragment, and therefore c ~ (\x xs -> x : toList xs) is its most general solution.

    So, toList must reduce to (\f -> f (\x xs -> x : toList xs) n) for some n. Clearly, toList can't have a normal form, since we can always unfold the recursive occurrence.