Oℕ
Я не знаю, можно ли в завтипном хаскеле делать абстракции, содержащие абстрактные пи-типы, если можно, наверное можно и бикатегорное какое-то выжать примитивное
Size: a a a
2020 August 02
AZ
круто, спасибо)
AG
понятно. Я просто думал что все несоответствие с теоркатом из-за всяких гадких боттомов, а тут различий оказалось ещё больше
для теорката нужно уметь законы формулировать, т.е. нужно достаточно мощное равенство
AG
в идеале да, уже для 1-категорий желательно что-то типа OTT
ЕО
Когда мы говорим "монада" в хаскеле, то подразумеваем монаду над "категорией" Hask, "линейная монада" будет монадой над другой категорией, каким-нибудь LinearHask, и т.д.
ЕО
Подозреваю, что с TypeInType можно было бы сформулировать какое-то обобщённое понятие монады, но нужно две вещи при этом понимать:
1. Это вообще не факт, что будет тоталится
2. Любое определение монады в хаскеле необходимое, но не достаточное. Мы верим программисту на слово, что законы выполняются
1. Это вообще не факт, что будет тоталится
2. Любое определение монады в хаскеле необходимое, но не достаточное. Мы верим программисту на слово, что законы выполняются
AZ
Подозреваю, что с TypeInType можно было бы сформулировать какое-то обобщённое понятие монады, но нужно две вещи при этом понимать:
1. Это вообще не факт, что будет тоталится
2. Любое определение монады в хаскеле необходимое, но не достаточное. Мы верим программисту на слово, что законы выполняются
1. Это вообще не факт, что будет тоталится
2. Любое определение монады в хаскеле необходимое, но не достаточное. Мы верим программисту на слово, что законы выполняются
во всяких идрисах насколько я знаю всякие VerifiedMonad тоже опциональны на случай "ну докажите если вам не трудно. А если трудно то и не нао"
ЕО
во всяких идрисах насколько я знаю всякие VerifiedMonad тоже опциональны на случай "ну докажите если вам не трудно. А если трудно то и не нао"
Идрис умеет быть тотальным, а хаскель нет
2020 August 03
Oℕ
Скажите, вот в compact closed category я для f: A -> B всегда могу объявить f*: B* -> A* так что f** = f
верно ли что
(f · g)* = g* · f* ?
верно ли что
(f · g)* = g* · f* ?
__
Скажите, вот в compact closed category я для f: A -> B всегда могу объявить f*: B* -> A* так что f** = f
верно ли что
(f · g)* = g* · f* ?
верно ли что
(f · g)* = g* · f* ?
могу ошибаться но это вроде как на braiding похоже
Oℕ
могу ошибаться но это вроде как на braiding похоже
Нет, braiding - это A (×) B -> B (×) A
Он естественно содержится в замкнутой категории, т.к. она симметрична
Он естественно содержится в замкнутой категории, т.к. она симметрична
Oℕ
Я спрашиваю, является ли звёздочка контравариантным функтором
Oℕ
а вот нашёл
Oℕ
но всё равно не очень понятно
2020 August 06
ЗП
как fix f = f (fix f) можно диаграммой отобразить?
AF
f = id?
к
тогда бы id и было, тут речь про произвольные f
VG
А что это за книга?
AK
А что это за книга?
Черновик Programming with Categories. Fond, Milewski, Spivak