История изменений

По теме - твоего кода я не понял (прошу прощения за мой хаскель... или это рекурсия банально? Так или иначе, я криво выразился, дело конечно не в error а в bottom), но да, тривиальная стрелка возможна из Void a -> Void b. Но она не возможна при маппинге объектов (т.е. a -> Void a, в общем случае из непустого множества в пустое), и хотя в хаскеле это и не нужно, но в теоркате - не функтор.

Хотя вот тоже, что считать за маппинг? Если мы возвращаем Void a для каждого a, то чем это собственно не маппинг объектов? Для маппинга стрелок множество не пустое, как ты упоминал, поэтому маппинг стрелок тоже есть. Выходит функтор.

знания агды на каникулах и попробовать там этот пруф сделать

Ничего не понял, но звучит очень круто! :) если руки дойдут, кинь ссылкой, пожалуйста, будь так добр.

По теме - твоего кода я не понял (прошу прощения за мой хаскель... или это рекурсия банально? Так или иначе, я криво выразился, дело конечно не в error а в bottom), но да, тривиальная стрелка возможна из Void a -> Void b. Но она не возможна при маппинге объектов (т.е. a -> Void a, в общем случае из непустого множества в пустое), и хотя в хаскеле это и не нужно, но в теоркате - не функтор.

знания агды на каникулах и попробовать там этот пруф сделать

Ничего не понял, но звучит очень круто! :) если руки дойдут, кинь ссылкой, пожалуйста, будь так добр.

знания агды на каникулах и попробовать там этот пруф сделать

Ничего не понял, но звучит очень круто! :) если руки дойдут, кинь ссылкой, пожалуйста, будь так добр.

По теме - твоего кода я не понял (прошу прощения за мой хаскель... или это рекурсия банально? Так или иначе, я криво выразился, дело конечно не в error а в bottom), но да, тривиальная стрелка возможна из Void a -> Void b. Но она не возможна при маппинге объектов (т.е. a -> Void a, в общем случае из непустого множества в пустое), и хотя в хаскеле это и не нужно, но в теоркате - не функтор.