5

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?

duplode
  • 33,731
  • 7
  • 79
  • 150
MaiaVictor
  • 51,090
  • 44
  • 144
  • 286
  • For that specific list, yes it exists. But you surely mean a function which can take _any_ such list, arbitrarily long, and returns a standard list, right? – chi Jun 02 '15 at 19:16
  • 1
    Yes, that is what I mean. – MaiaVictor Jun 02 '15 at 19:17
  • 2
    Shouldn't it be `\c n -> c 3 (\c n -> n)` in the end of the list? – András Kovács Jun 02 '15 at 19:57
  • 1
    The types of scott-encoded lists are not uniform - that is, the type changes each time you apply another "cons cell". You would need a type class to do this, otherwise the hypothetical `toList` function is ill-typed. – user2407038 Jun 02 '15 at 19:59
  • 1
    @user2407038 Indeed. I think this is more about the untyped lambda calculus than Haskell. – chi Jun 02 '15 at 20:08
  • @András, yes, thanks. – MaiaVictor Jun 02 '15 at 20:37
  • @chi well, someone convinced me ULC questions are still relevant to Haskell since that's still what you use when, for example, doing type-level computations, or writing DSLs. – MaiaVictor Jun 02 '15 at 20:39
  • 1
    I have a feeling that there's no such a term, but I have no idea about how to prove that. – chi Jun 02 '15 at 20:49
  • I agree. Intuitively, it doesn't make sense, indeed... but without a proof it is hard to know for sure. – MaiaVictor Jun 02 '15 at 20:50
  • 1
    Can't we do something with the fact that `newtype SList a = SList (forall r. r -> (a -> SList a -> r) -> r)` is not strictly positive? – András Kovács Jun 02 '15 at 21:24

1 Answers1

2

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.

András Kovács
  • 29,931
  • 3
  • 53
  • 99