История изменений

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. Это и будут частичные вычисления.

По-моему тут есть явная связь и есть смысл это совместить

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. Это и будут частичные вычисления