Хотелось бы, чтобы кто-то на семинаре рассказал, что такое refinement types, где и как они используются
Это типы, уточнённые предикатами. Например, type IntPos = {x : Int | x > 0}.
Пока, насколько я знаю, они поддерживаются, в основном, как расширения в некоторых языках. Например, Liquid Haskell, о котором упоминал @Rasie1.
В принципе, они ограниченно поддерживаются и в Паскале в диапазонных типах:
type My = 1..10;
только никто это не проверяет на этапе выполнения, поскольку это очень затратно
Диапазон это лишь малая часть предикатов, которые можно накладывать. Например, можно написать тип type Div3or5 = {v : Int | v mod 3 = 0 || v mod 5 = 0}
И — это проверяется на этапе компиляции, а не выполнения, SMT-солверами, которые умеют разрешать некоторые уравнения на некоторых типах (например, целые числа, списки).
Интересно, как это можно проверить на этапе компиляции…
var i: Div3or5
Read(i)
В любом случае должны быть проверки на этапе выполнения.
Да, действительно, согласна.
Впрочем, не вижу в этом проблемы. Если мы пишем функцию getNthElem из Int, то проверяем вручную, что пришедший на вход аргумент не отрицателен. А если аргумент типа Nat (где type Nat = {x : Int | x >= 0}), это делается автоматически, писать каждый раз проверку вручную не нужно.
Фишка в том, что можно более точно специфицировать код. Часть проверок берёт на себя компилятор. Например, можно написать функцию abs из Int в Nat, и компилятор выполнит проверку корректности реализации.
Ясно, что выразительные возможности предикатов ограничены тем, что умеют решать SMT-solvers. Но всё же типы с предикатами дают больше возможностей для написания более безопасного кода.
UPD Под более безопасным я имею в виду, что на этапе компиляции (статического анализа) отсекается больше ошибок времени выполнения.
1 лайк
А какие ограничения на условия налагаются чтобы SMT-солверы их могли тем не менее проверить? И насколько быстры такие проверки?
Я бы, конечно, советовал, если тема совсем незнакомая, немного готовиться к семинару, проводя хоть пол часика в Гугле… У нас не популярные лекции, которые предполагают простое и доступное изложение. Во всяком случае, понятно, что не все.
Refinement types это всё-таки types и вся наука здесь всё-таки о статических проверках. Приведу цитату из неплохого на первый взгляд туториала по ЛиквидХаскель, который упоминала Ю.В.:
By combining types with predicates you can specify contracts which describe valid inputs and outputs of functions. The refinement type system guarantees at compile-time that functions adhere to their contracts.
Вот простой затравочный пример (из статьи Refinement Types For Haskell — в соавторах один из отцов Хаскеля — С.П. Джонс)
type Pos = {v:Int | v > 0}
type Nat = {v:Int | v >= 0}
div :: n:Nat -> d:Pos -> {v:Nat | v <= n}
Вот такого рода контракты проверяются на этапе компиляции, используя упомянутые выше SMT-солверы. Вот про это наука.
Могу отметить также, что, скажем, в Хаскеле приведённый пример с Read вообще не имеет смысла. Вы накладываете ограничение на тип Int, а у введённой с клавиатуры величины совершенно другой тип (IO Int).
Я, кстати, посмотрел в Скопусе: за 2015 нашлось 12 статей о RT, в том числе в таких авторитетнейших изданиях, как
- Logical Methods in Computer Science,
- Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP, — 2 штуки
- Science of Computer Programming,
- Journal of Information Processing,
- ACM SIGPLAN Notices,
- ACM Symposium on Principles of Programming Languages.
Вот цитата из одной из статей с ICFP:
Refinement types allow the static verification of critical program properties
Насчёт Паскаля — хорошая шутка. Это типа как прийти на матанализ и сказать: о, знак суммирования в определении интеграла — да я его ещё в шестом классе изучал — какими тривиальными вещами вы тут занимаетесь…
1 лайк
Это наивные вопросы, на которые нет простых ответов. Всё зависит от конкретной системы, я думаю.
Может быть, нам стоит поискать того, кто сможет сделать отдельный доклад по SMT-солверам?
Это трудный вопрос, надо смотреть, кто что умеет. Это ж тоже целая наука… В википедии есть хорошая табличка про существующие SMT-solvers. Например, про Z3 написано следующее:
empty theory, linear arithmetic, nonlinear arithmetic, bitvectors, arrays, datatypes, quantifiers
Более конкретно сказать трудно, надо смотреть примеры.
Плюсую, это было бы интересно. Осталось найти специалистов по SMT!
Вот ещё цитата из статьи RT for Haskell про реальные задачи:
Our third contribution is an extensive empirical evaluation of our approach on more than 10, 000 lines of widely used complex Haskell libraries. We have implemented our approach in LIQUIDHASKELL, an SMT based verifier for Haskell. LIQUIDHASKELL is able to prove 96% of all recursive functions terminating, requiring a modest 1.7 lines of termination annotations per 100 lines of code, thereby enabling the sound, precise, and automated verification of functional correctness properties of real-world Haskell code
Есть учебный пример в том «туториале», на который я выше ссылался. Они там реализуют AVL-деревья и доказывают с помощью RT (LH), что всё правильно вставляется, удаляется и балансируется.
1 лайк
О, проверка завершимости это отличный пример, спасибо!
@Rasie1, это к вопросу о том, что можно требовать в качестве предикатов только завершающиеся алгоритмы. Я вот не знала, что можно проверять это средствами SMT, а хорошая штука.
1 лайк
Да, было бы замечательно послушать. Собирался разбираться с ними в ближайшие несколько недель, доклад бы ускорил это дело.
Эдак вы сами на доклад нарвётесь 
Институт математики, механики и компьютерных наук ЮФУ, 2005–2021