[
Size: a a a
Типы в языках программирования, моделирования, представления знаний и жизни
505 membersпожаловаться на группу
2022 January 24
a
insanely dependent types
a
менее формальные Self типы цедиля
a
которые я никогда блин не дочитаю
[
Я по завтипам только + и * верифицировал на лине
ПС
хм, а есть ли системы типов, в которых завтипы соседствуют с Тьюринг-полнотой?
в пруверах функции должны быть тотальными, в Idris тоже чекер тотальности...
в пруверах функции должны быть тотальными, в Idris тоже чекер тотальности...
[
У идриса есть нетотальный гиперсет
ПС
да это понятно, но можно ли использовать нетотальные функции в типах?
[
У хаскеля завтипы будут когда-нибудь
[
И у него уже нетотальный тайплевел
[
А вообще полнота по Тьюрингу не особо нужна
ПС
если прувать — безусловно
ПС
а вот если приложения писать...
ПС
там зачастую предполагается, что программа может никогда не завершиться