Всем привет. Хочу поделиться своим опытом использования библиотеки ProvingGround, написанной на Скале с использованием Shapeless. У библиотеки имеется документация, правда, не очень обширная. Автор библиотеки — Сиддхартха Гаджил из Indian Institute of Science. Библиотека экспериментальная. Сам Сиддхартха говорит, что это пока не библиотека, а «work in progress». Глобальная цель библиотеки — брать статью живого математика, парсить текст, переводить естественный язык с формулами в формальные доказательства, которые мог бы чекать компилятор. Понятно, что до этого еще очень далеко. Пока что в библиотеке можно работать с зависимыми типами и основами гомотопической теории типов (HoTT), (полу-) автоматически доказывать теоремы.
Читать полностью »
Рубрика «type theory»
От зависимых типов к гомотопической теории типов на Scala + Shapeless + ProvingGround
2017-05-22 в 9:11, admin, рубрики: dependent type, homotopy type theory, scala, type level programming, type theory, зависимые типы, математика, скала, типы данных, функциональное программированиеScala Moscow User Group, встреча 14 марта 2014
2014-03-05 в 9:15, admin, рубрики: functional programming, monads, scala, scalaz, tinkoff, type theory, Блог компании Тинькофф Кредитные Системы, функциональное программирование, метки: functional programming, monads, scala, scalaz, tinkoff, type theoryВ прошлый раз мы провели ознакомительную встречу. Собралось около 25 человек, мы узнали кто в Москве занимается разработкой на Scala и какие есть интересные проекты. Главной темой выбрали курс по реактивному программированию на Coursera, который как раз тогда подходил к концу.
В этот раз мы соберёмся послушать и обсудить два доклада:
- Алексей Иванов приедет из Питера и расскажет доклад «Monadic Bakery with Spray and Scalaz»,
про то почему Spray и ScalaZ — не страшные звери, а хорошие друзья; - Владимир Успенский расскажет про теорию типов и тем, как она связана с обычной разработкой в докладе:
«Теория типов, или как мы занимаемся математикой, программируя на Scala».
Доклады будут отнюдь не вводные, чуть глубже затронут тему функционального программирования и предназначены на подготовленных слушателей. После за чаем обсудим доклады, интересующие темы, а также планы на будущее.
Команда математиков за полгода написала 600-страничную книгу, используя GitHub
2013-06-26 в 16:58, admin, рубрики: agda, coq, Git, github, type theory, математика, перевод, переводы, метки: agda, coq, Git, github, type theory, математика, переводПеревод статьи Андрея Бауера — The HoTT book
Книга по HoTT закончена!
Начиная с весны, и даже раньше, я участвовал в командном проекте по написанию книги по гомотопической теории типов (Homotopy Type Theory). Она наконец написана и готова к употреблению. Вы можете скачать книгу бесплатно: homotopytypetheory.org/book/. Майк Шульман рассказал о содержании книги, так что я не буду повторять то же самое. Вместо этого я бы хотел прокомментировать некоторые социо-технологические аспекты создания книги и, в частности, рассказать о том, чему нас научило сообщество Open source.
Читать полностью »