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

[juan_gandhi]

It converges ok in a category with unlimited unions and finite products.

[chaource]

I doubt it. If it converges in that category, you would then have no trouble interpreting [[[x]]] = x.

[juan_gandhi]

Have to figure out. Need a Ramanujan.