Изменения

Лямбда исчисление с зависимыми типами {{---}} это такое расширение просто типизированного [[Лямбда-исчисление|лямбда-исчисления]], которое позволяет типам зависеть от значений. Например, в языке с таким исчислением функция может возвращать не просто пару чисел, а пару чисел, в которой первое число меньше второго, или если ваша функция принимает число <tex>n</tex> и возвращает массив длины <tex>n</tex>, то это можно будет выразить типом этой функции. Зависимые типы добавляют выразительности типовой системе, что приводит к лучшей проверке корректности программы на этапе компиляции. Однако, как показывает эта статья, для этого придётся идти на определённые жертвы: вам почти всегда придётся явно указывать типы ваших выражений, так как компилятор не сможет справится с выводом типов для них.