DS
теория типов Рассела
Она древняя как чёрт. Вон, посмотри на HoTT, CoC и т.п.
Size: a a a
2020 May 22
𝚙
теория типов Рассела фундаментально некорректна
p
потому что тебе сразу предьявят - кококо, это же определение из теории типов, ану давай кукарекай дальше на теориетипном
кто?
𝚙
я кстати что-то читал про HOTT
SP
тип это выражение заёбанности сигнатурками функций о которых ты знаешь что они принимают инты но это никак не выражено в их определении
AG
потому что тебе сразу предьявят - кококо, это же определение из теории типов, ану давай кукарекай дальше на теориетипном
Кто предъявит-то?
DS
теория типов Рассела фундаментально некорректна
Так речь не про неё, речь про современные теории типов такого плана.
𝚙
а вот про COC я не шарю
PP
что такое мощность типа?
кол-во их элементов
PP
у Bool например мощность 2
𝚙
Так речь не про неё, речь про современные теории типов такого плана.
я не очень хорошо разбираюсь в этом, но полагаю они имеют примерно те же недостатки
DS
теория типов Рассела фундаментально некорректна
Это всё равно, что ругаться на ZFC, вспоминая наивную теорию множеств
𝚙
раз не отказались от типа, как такового
SP
вы сейчас просто какой то бред говорите
𝚙
Это всё равно, что ругаться на ZFC, вспоминая наивную теорию множеств
нет ну она реально некорректна
𝚙
в любом языке
𝚙
Витгенштейн это исчерпывающе доказал
SP
ладно это намек что пора работать а не чатики читать
p
тип это выражение заёбанности сигнатурками функций о которых ты знаешь что они принимают инты но это никак не выражено в их определении
мда
AG
ладно это намек что пора работать а не чатики читать
И писать в них, возможно, тоже