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

[nivanych]

> Это что же значит, [[[a]]] = a?

Не равно, а изоморфно ;-)

[thedeemon]

Ну да, но в каком смысле трехмерный массив/список интов изоморфен одному инту, например?

[nivanych]

Извиняюсь, туплю, чотта в голове не так сложилось ;-)

шутка в делении

[sasha_gil]

Проглядывая преобразования по порядку - мне кажется, и минусу, и вынесению общего множителя за скобки можно придать смысл (пусть и трюками) в алгебре типов, но не делению.

[ext_4091418]

F(F(x)) не имеет разложения в нуле (= есть сколь угодно много списков списков A, не содержащих объектов типа A). После этого я ожидаю бредовый результат для G(F(F(x))) при любом G.

[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.

[os80]

>Это что же значит, [[[a]]] = a? ;)
Кажется, что между типами и многочленами / рациональными функциями существует не изоморфизм, а гомоморфизм (эпиморфизм?). И образ [[[a]]] под действием этого гомоморфизма совпадает с образом a. То есть [[[a]]] и a принадлежат к одному классу (т.е. имеют какие-то общие свойства, но какие - х.з.)
Ну а то, что с обычными списками так красиво получается - "просто повезло".