Oℕ
"только одна" значит что все остальные ей эквивалентны
ну да, если так, то понятно
хотя действительно, причем тут реализация на конкретном языке, с тз теории все в порядке
Size: a a a
2018 March 31
Oℕ
при чём
Oℕ
вполне при чём, повод вспомнить, что Hask - не категория
VY
ну вот я взял два различных языка и у них по-разному определен тип Void вообще,
можно ли сказать, что поэтому сравнивать реализации
вот я думаю, что раз отличаются определения типов и реализации инициальных и терминальных объектов, то сравнивать уже нельзя и это разные категории в разных языках
одна – Hask, другая – "Pursk" (например, лол) %)
можно ли сказать, что поэтому сравнивать реализации
absurd между ними будет не корректно?вот я думаю, что раз отличаются определения типов и реализации инициальных и терминальных объектов, то сравнивать уже нельзя и это разные категории в разных языках
одна – Hask, другая – "Pursk" (например, лол) %)
KV
вполне при чём, повод вспомнить, что Hask - не категория
Заворачиваение Void в обёртку как-то связано с нарушением категорных аксиом?
Oℕ
Заворачиваение Void в обёртку как-то связано с нарушением категорных аксиом?
кажется, да
Oℕ
повод вспомнить, как много разных способов есть получить различные между собой bottom
Oℕ
по сути в этом ведь они и нарушаются
KV
как можно это "интерпретировать" с тз тк?
в пурсе тo же:
должна же быть всего одна ф-ция
а оказывается их пару штук можно создать
(как бы странно это ни звучало, ну я понимаю что это к теории мало имеет отношения, это именно различия в "реализации")
absurd :: Void -> a
absurd a = case a of {}
в пурсе тo же:
newtype Void = Void Void
absurd :: forall a. Void -> a
absurd a = spin a
where
spin (Void b) = spin b
должна же быть всего одна ф-ция
absurd,а оказывается их пару штук можно создать
(как бы странно это ни звучало, ну я понимаю что это к теории мало имеет отношения, это именно различия в "реализации")
А это вообще откуда такое?
VY
верхняя ф-ция из Haskell, нижнее из PureScript
KV
Ну вот я про нижнее. В прелюдии Void определён как пустой тип, как и должно быть
KV
А ой
KV
VY
в общем я считаю что не корректно сравнивать разные категории из разных языков
ну т.е. корректно, но не так типа "я нашел 2 фции absurd в двух разных категориях"
ну т.е. корректно, но не так типа "я нашел 2 фции absurd в двух разных категориях"
Oℕ
Но можно и в одной
Oℕ
два существенно разных абсурда построить
VY
ооо, тогда это поломает же все, так же нельзя (с тз теории)
Oℕ
отсюда
https://wiki.haskell.org/Hask#Is_Hask_even_a_category.3F
https://wiki.haskell.org/Hask#Is_Hask_even_a_category.3F
r ~ ()
u1 r = case r of {}
u2 _ = ()
u1 undefined = undefined
u2 undefined = ()
VY
ну да, на практике можно, поэтому действительно определение с участием изоморфизма тут только справедливо
все, понятно
все, понятно