113
правок
Изменения
Лирическое вступление
Лямбда исчисление с зависимыми типами {{---}} это такое расширение просто типизированного [[Лямбда-исчисление|лямбда-исчисления]], которое позволяет типам зависеть от значений. Например, в языке с таким исчислением функция может возвращать не просто пару чисел, а пару чисел, в которой первое число меньше второго, или если ваша функция возвращает массив длины <tex>n</tex>, то это можно будет выразить типом этой функции. Зависимые типы добавляют выразительности типовой системе, что приводит к лучшей проверке корректности программы на этапе компиляции. Однако, как показывает эта статья, для этого придётся идти на определённые жертвы: вам почти всегда придётся явно указывать типы ваших выражений, так как компилятор не сможет справится с выводом типов для них.
==<tex dpi = "150">\lambda\Pi</tex>-исчисление==
{{Определение|definition=Множество '''термов''' (англ. ''term'') рекурсивно определяется следующей грамматикой:
