ну мы построили две не эквивалентных функции

хм, тогда не понятно
я почитаю пожалуй по ссылке сначала

И мне не понятно. В чём проблема-то?

ну ни в чём, просто Void - не инициальный объект

Почему?

потому что мы построили два существенно различных морфизма в объект ()

ну там вроде объясняется в этой статье в вики в подробностях почему вообще "Hask is not Cartesian closed"
я раньше не думал об этом "Actual Hask does not have sums, products, or an initial object, and () is not a terminal object"

А, я понял. Потому что днище в любом типе лежит

Ну, никто ж не запрещает не пользоваться днищем

запрещает

???

даже если выкинуть встроенные undefined и error

ты всегда можешь построить runIndentity $ forever $ return ()

Честно говоря, я могу себе разрешить и этим тоже не пользоваться

компилятор это выражение типизирует, значит, ты всегда должен рассчитывать на возможность дна в любом месте

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

я к этому вопросу из лекций Бартоза пришел, по тк когда объяснялось почему a^0 = 1:
"В Haskell, мы заменяем 0 на Void, 1 на единичный тип (), а экспоненциал на функциональ- ный тип. Утверждается, что множество функций от Void к любому типу а эквивалентно единичному типу, который является синглетоном. Другими словами, существует только одна функция Void -> а. Мы уже сталкивались с этой функцией: она называется absurd."

сначала напрягло "только одна" и вот отсюда пошли эти не здоровые мысли :)
да, пожалуй с использованием аналогий из этих языков нужно просто всегда держать в голове эти оговорки и не париться :)

Эх, вот бы у меня был тоталити-чекер

ну в общем, если не загоняться по поводу боттома и MonadFix Identity нет никаких проблем

Но пример из PureScript же всё равно ни о чём не говорит?