AC
Size: a a a
Типы в языках программирования, моделирования, представления знаний и жизни
505 membersпожаловаться на группу
2022 January 24
[
А ограничение рекурсии в языках с завтипами нужно потому что там термы в типы проваливаются?
ПС
Сорян, некорректно выразился из-за того, что в хаскельном rfc говорят про term-level syntax и type-level syntax
AC
Грубо говоря, Type Soundness = Type Preservation + Progress. Так что если зацикливающееся вычисление не меняет свой тип (Progress тут очевиден) — всё полностью sound.
[
Капец, звучит так, будто мне всё же надо прочитать что-то по теории типов
AC
Не проваливаются, а поднимаются. 😁
[
Я просто на всё смотрю вверх ногами
ПС
Ещё и от противного доказываете, небось
AC
Да нет, я просто хотел уточнить, какой именно кейс Вы имеете в виду?
ПС
Когда для вычисления типа нужно произвести потенциально не завершающееся вычисление
AC
Все доказательства от Кролика — доказательства от противного. 🤣
Извините... 😅
Извините... 😅
ПС
Вот в предположении, что все эти вычисления таки завершаются, разве soundness ломается?
AC
Да, soundness ломается именно тогда, когда мы предполагаем, что все вычисления завершаются, а они не завершаются. На этом можно сделать type confusion aka unsafe coerce.
ПС
Блин, а, казалось бы, компляция либо не завершается, либо завершается корректно...