Еще больше злоупотребляя алгеброй алгебраических типов данных - почему это работает?

Итак, я читал, как вы можете преобразовать ADT в то, что напоминает вещественные числа, и манипулировать ими на таких страницах, как этот вопрос SO и эта серия из трех частей и особенно это .

Мое внимание привлек раздел "Проблемы" последней ссылки, и я попытался решить Nat в нем, хотя в статье говорится, что это невозможно.

Nat = 1 + Nat
Nat - Nat = 1
Nat(1 - 1) = 1
Nat = 1 / (1 - 1)

Это может показаться полной ерундой, поскольку я просто разделил на 0 (и, возможно, вы правы), но если вы прочитаете любую из этих ссылок или что-то подобное, вы заметите, что это очень похоже на определение списка.

List(x) = 1 / (1 - x)

Таким образом, вы можете написать Nat как Nat = List(1) = 1 + 1 + 1 + ..., и это именно то, что вы получили бы, повторяя подстановку в исходном уравнении. Это также эквивалентно определению таких натуральных чисел в Haskell:

type Nat = [()]

Это определенно допустимая кодировка натуральных чисел, где 0 = [] и S(N) = () : N.

Итак, мой вопрос в том, как же я получил из этого достоверный результат? Я просто разделил на ноль. Не говоря уже о самом исходном уравнении, в значительной степени противоречащем друг другу.

Так почему же я получил что-то, что имеет смысл в конце этого? Это просто чистое совпадение или деление на 0 каким-то образом определено в этом контексте, что имеет смысл?


haskell algebraic-data-types
person The Red Fox    schedule 28.09.2016    source источник
comment
Собственно говоря, 1 != 1*1, поэтому правильнее было бы написать Nat = 1 + 1*1 + 1*1*1 + ....   -  person chepner    schedule 28.09.2016
comment
@chepner, пожалуйста, объясните почему? В моем понимании типы образуют полукольцо, где 1 - это идентичность *. Другими словами x * 1 = 1 для любого x. Итак, 1 и 1*1 эквивалентны.   -  person The Red Fox    schedule 28.09.2016
comment
Они изоморфны, но не эквивалентны. Упорядоченная пара ((), ()) отличается от (). x * 1 == x, потому что вы можете без потерь преобразовать значение (a, ()) :: (x,()) в a :: x и наоборот.   -  person chepner    schedule 28.09.2016
comment
@chepner, все эти манипуляции в любом случае (в лучшем случае) до изоморфизма. Просто прочтите =, поскольку он изоморфен, если хотите.   -  person Reid Barton    schedule 28.09.2016
comment
Я думаю, ответ, вероятно, заключается в том, что вы выполняли только манипуляции, которые вы также могли бы сделать с помощью List (x), но написали 1 вместо x. Но мне непонятно, есть ли здесь реальный вопрос.   -  person Reid Barton    schedule 28.09.2016

Ответы (1)


arrow_upward
1
arrow_downward

Поскольку Nat бесконечно, вы не можете использовать Nat - Nat = Nat ⋅ (1 - 1) = Nat ⋅ 0 = 0. Разница Nat - Nat - это как бы некоторое конечное число, тогда как Nat, очевидно, бесконечно. Таким образом, 1 - 1 на самом деле не ноль, это скорее как бесконечно малое значение в нестандартном анализе . Если вы разделите что-то на бесконечно малое, вы получите что-то расходящееся большое (действительно бесконечное ... да), но вы не попадете точно в деление на ноль.

Фактически, я думаю, что этот парадокс, о котором вы спрашивали, можно было бы рассматривать как «доказательство того, что Nat бесконечен» - потому что, если бы он был конечным, вы делили бы на ноль.

Разумеется, вы не можете доказать что-либо с помощью такой арифметики типов ... это занимательное времяпрепровождение, но не совсем правильная математика.

person leftaroundabout    schedule 28.09.2016
comment
Не с этой сортировкой, нет, но с более тщательной сортировкой (метод разностного исчисления) вы, безусловно, можете. - person dfeuer; 28.09.2016