TN
data Core = U | Stream | Pi | Lam | App | Fix
Size: a a a
2017 November 21
AK
Я могу попробовать рассказать, какие у меня есть на эту тему интуиции и откуда они растут, но во-первых растут они из теорфизики и будет не шибко понятно, а во-вторых, заранее попрошу математиков не кидаться тапками, потому что это такие очень примерные физические интуиции, и если их понимать слишком дословно, то будет казаться, что я порю полную чушь.
AK
Нет, линейные типы, которые получаются из языка Stream — это очень узкое понимание линейных типов. Самого интересного (типа линейного Unit-типа, который спектр сфер) там не будет.
NK
Ну не бывает такого чтобы не было статей. Если нет решений - должна быть формулировка проблем хотя бы, или упрощённые решения (для аффинных логик например).
TN
Ну Stream пример, можно как носитель брать HIT рекурсивный, тот же стрим
TN
например инфинити-групоид
TN
он же тоже стрим :-)
TN
сравнение стримов, бисимуляция
TN
это и есть отношение эквивалентности и Path-тип для стримов
AK
ID:402926333
Ну не бывает такого чтобы не было статей. Если нет решений - должна быть формулировка проблем хотя бы, или упрощённые решения (для аффинных логик например).
https://ncatlab.org/nlab/show/dependent+linear+type+theory — тут есть вся библиография по вопросу.
AK
это и есть отношение эквивалентности и Path-тип для стримов
Откуда там возмётся спектр сфер?
TN
А можешь на задаче объяснить?
AK
А можешь на задаче объяснить?
Я вам счас за**ру весь чат непонятной хренью. Точно надо? 😊 Я-то с удовольствием, но...
TN
или последовательность спектров и условный стрим показать
TN
так чтобы ВСЕ поняли )
NK
https://ncatlab.org/nlab/show/dependent+linear+type+theory — тут есть вся библиография по вопросу.
Премного благодарен, на большее я не рассчитывал. На нкатлабе почему-то не догадался посмотреть, а гугл слишком плохую выдачу выдавал
AK
Так чтобы все поняли я пока сам не понимаю. 😊
TN
я согласен на всё
TN
рассказывай что знаешь!
NK
Я вам счас за**ру весь чат непонятной хренью. Точно надо? 😊 Я-то с удовольствием, но...
Точно надо! Я тоже согласен!