.title-slide # Система typestate в языке Rust .right[Андрей Власовских] .right[JetBrains] --- .title-slide # #fprog --- # О докладчике * Андрей Власовских * http://pirx.ru/ * @vlasovskikh * JetBrains * PyCharm — IDE для Python * ФП * СПб Политех, SPbHUG, FProg --- # Язык Rust * Mozilla Labs, v0.3 * Характеристики * Системный * **Безопасный** * Функциональный * Объектно-ориентированный * Для крупных проектов --- # Typestate в Rust * Статически проверяемые состояния типов, в которых разрешены некоторые операции с ними fn head
(v: &[T]): is_not_empty(v) -> T; * Статические гарантии языка * Инициализированные переменные * Безопасные указатели на изменяемую память между потоками --- # План * Введение * .current[Обзор Rust] * .next[Typestate] * .next[Неинициализированные переменные] * .next[Статья о typestate] * .next[Typestate в Rust] --- .title-slide # Обзор Rust --- # Системный * Статическая типизация * Контроль над памятью * Взаимодействие с C --- # Безопасный * (Опять) Статическая типизация * Многозадачность через обмен сообщениями * Можно передавать изменяемую память * Нет null и NPE * Нет неинициализированных переменных * Нет исключений, цепочка задач * Больше гарантий через typestate --- # Функциональный * Неизменяемые данные по умолчанию * Добавление `mut` создаёт новый тип * Функции высшего порядка, замыкания * Разные виды по соображениям эффективности * Алгебраические типы и сопоставление с образцом * Параметрические типы, классы типов --- # Объектный * Изменяемое состояние * Локальное, в структурах, классах, задачах * Интерфейсы * Реализация отдельно от объявления интерфейса и типа * Можно делать extension methods --- # Крупные проекты * Явные импорты имён как в Python * Компиляция и зависимости на уровне сборок * Сборка (crate) — единица компиляции, группа файлов * Система пакетов --- .title-slide # Typestate --- # Неинициализированная переменная (1) fn f(c: bool) -> int { let p: ~int; if c { p = ~14; } // Нет присваивания в else ret *p; } --- # Неинициализированная переменная (2) fn f(c: bool, d: bool) -> int { let p: ~int; // Статически нельзя сказать, что бесконечный // loop { ... } -- бесконечный while c { if d { p = ~14; break; } } ret *p; } --- # Граф потока управления .rust fn f(c: bool, d: bool) -> int { Write c let p: ~int; Write d while c { While <--+ if d { Read c ---|-+ p = ~14; If | | break; Read d ---+ | } Write p | } Break | ret *p; Return <----+ } Read p --- # Полурешётка {c,d,p} / | \ / | \ / | \ {c,d} {c,p} {d,p} | \ / \ / | | \/ \/ | | /\ /\ | | / \ / \ | {c} {d} {p} \ | / \ | / { } * Полурешётка * Множество: множества имён переменных * Отношение частичного порядка: включение множеств * Наибольшая нижняя грань: пересечение множеств --- # Анализ потока данных Write c {c} {c} {c} Write d {c,d} {c,d} {c,d} While <--+ {c,d} {c,d} {c,d} Read c ---|--+ {c,d} {c,d} {c,d} If | | {c,d} {c,d} {c,d} Read d ---+ | {c,d} {c,d} {c,d} Write p | {c,d,p} {c,d,p} {c,d,p} Break | {c,d,p} {c,d,p} {c,d,p} Return <-----+ {c,d,p} {c,d} {c,d} Read p {c,d,p} {c,d} {c,d} {c,d,p} & {c,d} = {c,d} // Наибольшая нижняя грань --- # Typestate (1) * Статья 1986 года * R. Strom, S. Yemini. Typestate: A Programming Language Concept for Enchancing Software Reliability * Обогащение понятия типа * Тип определяет разрешённые операции над объектом, а состояние типа (typestate) — разрешённые операции в конкретном контексте --- # Typestate (2) * Обобщение алгоритма поиска неинициализированных переменных * (Более) Произвольная решётка со своим
блэкджеком
множеством и отношениями * Можно статически найти бессмысленные операции * Нулевые указатели, не- и де-инициализированные переменные, обращения за границы массивов и пр. --- # Typestate в Rust * В компиляторе * Неинициализированные переменные * Отправленные другой задаче указатели * Пользовательские * Предикаты `pure fn` и инструкции проверки состояния `check` * Ограниченная возможность задания своей решётки --- # Read и Write на псевдокоде typestate .rust pure fn init
(x: T) -> bool { ... } // Read fn read
(x: T): init(x) -> T { ... } // Write x = ...; check init(x); // Пример let p: ~int; if ... { p = ~14; check init(p); } return *(read(p)); --- # Решётка состояний типов * Определение * Множество: множества кортежей _(pred, name1, name2, name3, ...)_ * Порядок: отношение включения pure fn init
(x: T) -> bool { ... } pure fn positive(x: int) -> bool { ... } let (x, y): (int, int); top: {(init,x), (init,y), (positive,x), (positive,y)} bottom: {} --- # Пользовательский предикат pure fn positive(int x) -> bool { x > 0 } fn get
(xs: &[T], int i): positive(i) -> T { xs[i] } fn f() { let mut i: int = ...; let xs: ~[str] = ...; check positive(i); io::println(get(xs, i)); // Хорошо i = ...; io::println(get(xs, i)); // Плохо } --- # Условная проверка fn get
(xs: &[T], int i): positive(i) -> T { xs[i] } fn f() { let mut i: int = ...; let xs: ~[str] = ...; if check positive(i) { io::println(get(xs, i)); // Хорошо } } --- # Ссылочная прозрачность * Ограничения на предикаты * Запрещены присваивания * Запрещены рекурсивные вызовы * Запрещены не `pure` функции * (Не) Запрещены типы с `mut` частями * Можно обойти pure fn side_effects_may_include
(x: T) -> bool { unchecked { ... } } --- # Использовавшиеся в Rust предусловия pure fn is_even(int x) -> bool; pure fn positive(int x) -> bool; pure fn nonnegative(int x) -> bool; pure fn le(int a, int b) -> bool; pure fn vec::is_not_empty
(v: &[T]) -> bool; pure fn vec::same_length
(xs: &[T], ys: &[U]) -> bool; pure fn starts_with(s: str, pred: str) -> bool; ... --- # Typestate в отправке сообщений fn main() { let port = comm::port(); let chan = comm::chan(port); do task::spawn { let msg: ~mut bool = ~mut true; io::println(#fmt("%b", *msg)); // Хорошо comm::send(chan, msg); io::println(#fmt("%b", *msg)); // Плохо } let result = comm::recv(port); io::println(#fmt("%b", *result)); } --- # Typestate в Rust больше нет? * В Rust > 0.3 убрали из языка * Пользовательский typestate не был полезен * Не поддерживались постусловия в функциях * Проверка типов без изменяемых полей * Но внутри алгоритмы остались * Неинициализированные переменные * Передача изменяемой памяти между задачами очень крута --- .center.middle # Вопросы? http://pirx.ru/ @vlasovskikh