Overly algebraic

[thedeemon]

Вот список имеет вид
data List a = Nil | Cons a (List a)
т.е.
F(x) = 1 + x * F(x)
а значит
F(x) - x * F(x) = 1
(1-x) * F(x) = 1
F(x) = 1 / (1-x)
и действительно, если мы такую функцию разложим в ряд, то получим
F(x) = 1 + x + x*x + x*x*x + x*x*x*x + ...
т.е. как раз тип описывает списки из х разной длины.

Но вот что любопытно,
F(F(F(x))) = 1 / (1 - (1 / (1 - 1 / (1 - x)))) = ... = x
можете на бумажке проверить или вот тут увидеть.
Это что же значит, [[[a]]] = a? ;)

Comments

[sassa_nf]

Well, if we follow the rabbit hole far enough, we end up with a requirement that may not hold in arbitrary categories?

Eg what is "-x"? If we were to apply algebra directly, it is such a type y such that x+y=0. I think non-trivial types never add up to 0, so "-x" cannot be defined for arbitrary categories.

[juan_gandhi]

See, you don't need negation. All you have is a property of a series, the equation that it satisfies.

[sassa_nf]

I am not certain of that. First you need to ensure that division does not introduce undefined.

Say, F(x)=1+x*F(x) holds for all x, including x=1. Then F(x)-x*F(x)=1 - is this still so for x=1? There are infinities involved, so it's beyond my level of understanding how to do the subtraction in such a way that the difference is 1 (and, say, not 0, and not 2). Maybe not only Ramanujan knows.

Or is (1-x)*F(x)=1? Even for x=1? Why is it ok to divide by (1-x)? Before we get to representation of 1/(1-x) as a series.