Oℕ
Опять же в достаточной степени ограниченная категория Idr будет чрезвычайно похожа на в достаточной степени ограниченную категорию Hask
Size: a a a
2020 February 12
ЕО
Идрис же нетьюринг-полный, у термов идриса есть нормальная форма. Так что несложно построить Idr (легче чем Hask), типы это объекты, а стрелки — нормальные формы термов. Композиция определена через нормальную форму терма a . b
Oℕ
Идрис же нетьюринг-полный, у термов идриса есть нормальная форма. Так что несложно построить Idr (легче чем Hask), типы это объекты, а стрелки — нормальные формы термов. Композиция определена через нормальную форму терма a . b
Тьюринг полный, если захотеть
Oℕ
Тоталити чеккер опциональный
Oℕ
Тотальность - атрибут функции
ЕО
Тьюринг полный, если захотеть
Ну так и про агду и даже кок сказать можно
ЕО
Нетотальный идрис это что-то типа unsafe {} в расте
Oℕ
Не
Но в идрисе специально сделано.
Т.е. там ядро поддерживает не только тотальные функции
Но в идрисе специально сделано.
Т.е. там ядро поддерживает не только тотальные функции
Oℕ
Т.е. ты вполне можешь накатать кучу функций без %default total
Oℕ
Т.е. total - это такой киворд как const в C++, можно спокойно без него писать
МБ
Не знаю, в тему ли, но в категории Vect произведение совпадает с копроизведением, а инициальный объект {0} совпадает с терминальным. И, вроде, ok. Поэтому, вроде как, пока из Void ведёт только по одной стрелке в другие типы, ничего не мешает ему быть инициальным объектом.
МБ
Проблема Hask, насколько я понимаю Брауэра не в том, что он Тьюринг-полный, а в том, что там есть
seq, который ломает всю красоту. Если взять Haskell без seq, то всё будет хорошо.NI
Не знаю, в тему ли, но в категории Vect произведение совпадает с копроизведением, а инициальный объект {0} совпадает с терминальным. И, вроде, ok. Поэтому, вроде как, пока из Void ведёт только по одной стрелке в другие типы, ничего не мешает ему быть инициальным объектом.
> в категории Vect произведение
С точки зрения теории типов, нам в этой категории интереснее тензорное произведение ⊗, дуальное к нему ⅋ и комбинации типа A* ⅋ B ;-)
С точки зрения теории типов, нам в этой категории интереснее тензорное произведение ⊗, дуальное к нему ⅋ и комбинации типа A* ⅋ B ;-)
МБ
> в категории Vect произведение
С точки зрения теории типов, нам в этой категории интереснее тензорное произведение ⊗, дуальное к нему ⅋ и комбинации типа A* ⅋ B ;-)
С точки зрения теории типов, нам в этой категории интереснее тензорное произведение ⊗, дуальное к нему ⅋ и комбинации типа A* ⅋ B ;-)
Ну, да, ну, да. Квантовые компьютеры... МмммМм. Сам ещё не смотрел, может и мура, но докладчик, вроде, очень продвинутый дядька.
https://youtu.be/3QpPj_raMps
https://youtu.be/3QpPj_raMps
NI
Ну, да, ну, да. Квантовые компьютеры... МмммМм. Сам ещё не смотрел, может и мура, но докладчик, вроде, очень продвинутый дядька.
https://youtu.be/3QpPj_raMps
https://youtu.be/3QpPj_raMps
Аффтар известный, у него немало хороших статей.
Например, про конкурентную семантику линейных типов.
Выступление не видел.
Например, про конкурентную семантику линейных типов.
Выступление не видел.
ЗП
вроде как все это в розетском камне описано
МБ
Там больше про струны и топологии. А тут более приземлённые вещи заголовок обещает. Но, может, и то же самое.
ЗП
кстати было бы круто увидеть более современную версию RS
ЗП
там не только про струны и топологию
ЗП
и логику и фп и прочее