Системы типов — это настоящее безумие.
Некоторое время назад я уже отметился здесь со статьёй, в которой пытался разобрать, какие гарантии в compile-time может дать система типов Rust. Кое-какие интересные моменты удалось выловить уже тогда, однако больше всего меня зацепил весьма развёрнутый комментарий, описывающий некоторые вещи, доступные в зависимо-типизированном Idris.
Разумеется, я не мог остаться в стороне. Результат исследований доступен на github, а детальный разбор — под катом.
В Serokell мы занимаемся не только коммерческими проектами, но стараемся изменить мир к лучшему. Например, работаем над улучшением главного инструмента всех хаскелистов – Glasgow Haskell Compiler (GHC). Мы сосредоточились на расширении системы типов под впечатлением от работы Ричарда Айзенберга "Зависимые типы в Haskell: теория и практика".
В нашем блоге Владислав уже рассказывал о том, почему в Haskell не хватает зависимых типов и как мы планируем их добавить. Мы решили перевести этот пост на русский, чтобы как можно больше разработчиков могло использовать зависимые типы и сделать дальнейший вклад в развитие Haskell как языка.
Привет. На днях я искал, как сделать что-то в Idris, и наткнулся на неплохой пост, вольный перевод которого выглядит вполне уместным. Вольности и отсебятину, где необходимо, я буду обозначать ⟦вот такими закорючками в начале и в конце⟧.
Когда стоит использовать тесты, а когда — типы? Какую информацию и какие гарантии мы получаем в обмен на наши усилия по их написанию?
Мы рассмотрим простой и немного надуманный пример, выраженный на Python, C, Haskell и Idris. Мы также увидим, что можно сказать о реализации без каких-либо дополнительных знаний о ней, в каждом из случаев.
Мы не будем учитывать разнообразные чёрные ходы, позволяющие явно нарушать гарантии языка (например, расширения C, unsafePerformIO в Haskell, небезопасные приведения типов), иначе нельзя было бы сделать вообще никаких выводов, и этот пост получился бы довольно коротким. ⟦Кроме того, у того же хаскеля есть подмножество Safe Haskell, явно и транзитивно запрещающее использование этих и ряда других трюков, могущих нарушить целостность языка.⟧
Не так давно на Хабре перевели статью о том, как при помощи алгебраических типов данных добиться того, чтобы некорректные состояния были невыразимыми. Сегодня мы посмотрим на чуть более обобщённый, масштабируемый и безопасный способ выражать невыразимое, а поможет нам в этом хаскель.
Model-Updater-View — функциональный паттерн, успешно применяемый в языке Elm в основном для разработки пользовательских интерфейсов. Что бы им воспользоваться надо создать тип Model, представляющий полное состояние программы, тип Message, описывающий события внешней среды, на которые программа должна реагировать, меняя свое состояние, функцию updater, которая из старого состояния и сообщения создает новое состояние прораммы и функции view, которая вычисляет по состоянию программы требуемые воздействия на внешнюю среду, которые порождают события типа Message. Паттерн очень удобный, но у него есть маленький недостаток — он не позволяет описать какие собятия имеют смысл для конкретных состояний программы.
Схожая проблема возникает (и решается) и при использовании ОО-паттерна State.
Язык Elm простой, но очень строгий — он проверяет, что функция updater хоть как-то обрабатывает все возможные сочетания модели-состояние и сообщения-события. По этому приходится писать лишний, пусть и тривиальный — как правило оставляющий модель без изменений, код. Я хочу продемонстрировать, как этого можно избежать в более сложных языках — Idris, Scala, C++ и Haskell.
Читать полностью »
Всем привет. Хочу поделиться своим опытом использования библиотеки ProvingGround, написанной на Скале с использованием Shapeless. У библиотеки имеется документация, правда, не очень обширная. Автор библиотеки — Сиддхартха Гаджил из Indian Institute of Science. Библиотека экспериментальная. Сам Сиддхартха говорит, что это пока не библиотека, а «work in progress». Глобальная цель библиотеки — брать статью живого математика, парсить текст, переводить естественный язык с формулами в формальные доказательства, которые мог бы чекать компилятор. Понятно, что до этого еще очень далеко. Пока что в библиотеке можно работать с зависимыми типами и основами гомотопической теории типов (HoTT), (полу-) автоматически доказывать теоремы.
Читать полностью »
Computer Science клуб вот уже 10 лет проводит открытые курсы по компьютерным наукам. Большинство этих лекций стараниями Лекториума записаны на видео и лежат в открытом доступе. В этом семестре выложены уже три новых курса, которые до этого не читались в клубе: «Программирование с зависимыми типами на языке Idris», «Вычисления на GPU. Основные подходы, архитектура, оптимизации», «Методы и системы обработки больших данных».
Читать полностью »
Шаблоны проектирования! Впервые я узнал о них на курсе Software Design, когда учился в магистратуре Академического университета. Мы писали различные программы на Java с использованием шаблонов. С тех пор это словосочетание ассоциируется у меня с чем-то таким ООПшным. Однако, разбираясь с языком Agda, я наткнулся на статью The Power Of Pi, которая рассказывает про шаблоны проектирования в языках с зависимыми типами!
В этом посте я хочу рассказать об одном из этих шаблонов, который называется View. С его помощью можно реализовывать пользовательские правила pattern matching'a. Если вам интересно, что это за шаблон, что такое пользовательский pattern matching, каковы особенности pattern matching'а в языках с зависимыми типами, и вы знакомы с каким-нибудь функциональным языком программирования со статической типизацией (Haskell, Scala, Ocaml, F#) — добро пожаловать под кат!Читать полностью »
