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

[deniok]

Это не порождает при обратной сборке рекурсивного уравнения, вот в чем беда: 1 + x * F(F(x)) = x.