Исправление SZT, (текущая версия) :
Refinement type — это когда ты объявляешь, что функция, принимающая векторы длиной M и N вернёт вектор длиной M + N, где M и N задаются в рантайме, а компилятор тебе в compile time проверяет доказательство, что твоя функция именно так себя ведёт.
Ну вообще-то я б не сказал. Вот допустим есть у нас функция concat(a,b), принимающая векторы a, b и возвращающая c. Если мы потом где-то в коде программы сравниваем veclen(a) <= veclen(c) то компилятор может эту проверку выкинуть, заменив на true т.к. из свойств функции concat и истории жизни переменных a, c следует, что сравнение veclen(a) <= veclen(c) обязательно вернет true. Это и будут частичные вычисления.
По-моему тут есть явная связь и есть смысл это совместить
Исходная версия SZT, :
Refinement type — это когда ты объявляешь, что функция, принимающая векторы длиной M и N вернёт вектор длиной M + N, где M и N задаются в рантайме, а компилятор тебе в compile time проверяет доказательство, что твоя функция именно так себя ведёт.
Ну вообще-то я б не сказал. Вот допустим есть у нас функция concat(a,b), принимающая векторы a, b и возвращающая c. Если мы потом где-то в коде программы сравниваем veclen(a) <= veclen(c) то компилятор может эту проверку выкинуть, заменив на true т.к. из свойств функции concat и истории жизни переменных a, c следует, что сравнение veclen(a) <= veclen(c) обязательно вернет true. Это и будут частичные вычисления