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

Comments

[kodt_rsdn]

Алгебра типов - не группа и не кольцо. Более того, Nil не является нейтральным элементом ни по сложению, ни по умножению.
Поэтому заменить его на 1 - это слишком смело.
1*1*1 = 1, nil*nil*nil ≠ nil. (список из двух пустых списков и терминатора).
Вот эта ситуация, когда nil может быть самостоятельным значением, а может терминатором, портит малину.

Иначе, если мы говорим, что квадратные скобки раскрываются так же, как круглые, то конечно, в расплющенном списке форма равна содержанию.

[thedeemon]

Ну зачем же так громко в лужу.
1 это довольно стандартное обозначение терминального объекта категории, и все типы с единственным значением принято обозначать 1, они все друг другу изоморфны. У типа 1*1*1 (тупл из трех юнитов) тоже единственное значение, и потому тип 1*1*1 изоморфен 1, т.е. 1*1*1=1. Про значение списка из трех элементов мы тут не говорим, мы говорим про типы.
Вот что это не группа и не кольцо, это да. Нормального вычитания и деления там нет, и когда какие-то результаты таких преобразований дают осмысленные предсказания, это самое удивительное.
Квадратными скобками у меня как в хаскеле и еще ряде языков обозначен тип списка, т.е. [А] это список из элементов типа А, а [[[A]]] это трижды вложенный список из А.

[kodt_rsdn]

Не, секунду! N-мерные векторы или кортежи таки имеют нейтральное значение, но список - это нечто не фиксированного размера, [[],[],[]] не изоморфен [[]].

Ну и nil - это так себе единичка. А если у нас два терминальных объекта:
List a = Foo | Bar | Cons a (List a)
тогда что? 1+1+x*f(x) ?

[thedeemon]

Опять путаем значения и типы? [[],[],[]] и [[]] это два значения одного и того же типа. 4 это не 5, но оба инты.

Да, "List a = Foo | Bar | Cons a (List a)" это 1+1+x*f(x).
Тот же Bool = True | False известен как 2 = 1+1.

[kodt_rsdn]

Про скобки я понимаю. Я как раз хотел сказать, что у них несколько разная семантика, список сам по себе не выполаживается, поэтому и проецировать его на арифметику - странно.

[kodt_rsdn]

Ну а то, что предсказания осмысленные, - это может быть стстематично (какие-то изоморфизмы или около того), а может быть забавный анекдотец и случай. Как с фокусами вокруг умножения на ноль.