Lambda World 25 — Вдохновители refinement types: Хорхе Майораль и Хуанхо Мадригал

Должна ли ваша функция принимать только положительные целые числа? Всегда ли она возвращает непустые списки? Уточняющие типы — это замечательно: помимо типизации, вы можете аннотировать поведение значений вашей функции. Это отличный союзник для корректности программы, но есть нюансы: очевидно, что проверка должна выполняться не во время выполнения, а во время компиляции, и это может быть нетривиальной задачей. Нам нужен мозг, главный разработчик, который учитывает все условия и проверяет нашу программу. И чтобы это работало, этот главный разработчик должен умело комбинировать множество компонентов: зависимые типы, логику, полиморфизм... очень интересный хаос. В этом докладе мы хотим интуитивно и на примерах представить этих главных разработчиков, решатели SMT (Satisfiability Modulo Theories) и их применение к семантическому обогащению многих языков программирования, как это происходит с решателем Z3 в Liquid Haskell, и сравнить подход уточняющих типов с подходом зависимых типов, как это происходит с Idris, Agda или Lean.