Летняя школа в г.Оксфорд 2015 — различия между версиями

Версия 20:54, 25 июля 2015

Библиотека колледжа Сэн Энн, в котором проводилась школа

Летняя школа в Оксфордском университете проходила с 6 по 10 июля 2015 года, лекции читались 4 и ¼ дня, по 4 лекции в день. Официальное название: Summer School on Generic and Effectful Programming (Летняя школа по обобщённому программированию и программированию с вычислительными эффектами). Непосредственной организацией занимались профессора Р. Хинзе и Дж. Гиббонс. Официальная точка входа к материалам школам расположена на сайте школы. Однако на всякий случай материалы продублированы (и местами дополнены заметками и релевантными статьями) на нашем сервере. Ниже приведён список курсов лекций с карточками лекторов и комментариями.

Организаторы школы, оксфордские профессора Джереми Гиббонс Ральф Хинзе

Контейнеры для эффектов и контекстов (Т. Уусталу)

Лектор

Тармо Уусталу

Место работы: Институт кибернетики Талиннского университета технологии.

Тема диссертации: Natural Deduction for Intuitionistic Least and Greatest Fixedpoint Logics, with an Application to Program Construction, 1998, Stockholm.

Основные публикации

• Type-based termination of recursive definitions, 2004, coauth. Barthe, Frade, Giménez, Pinto // Mathematical Structures in Computer Science 14 (01), pp. 97-141. Cit. 95.
• Primitive (Co) Recursion and Course-of-Value (Co) Iteration, Categorically, 1999, coauth. Vene // Informatica, Lith. Acad. Sci. 10 (1), pp. 5-26. Cit. 78.
• Iteration and coiteration schemes for higher-order and nested datatypes, 2005, coauth. Abel, Matthes // Theoretical Computer Science 333 (1), pp. 3-66. Cit. 53.

Недавние публикации

• Certified CYK parsing of context-free languages, 2014, coauth. Firsov // Journal of Logical and Algebraic Methods in Programming 83 (5), pp. 459-468.

Содержание

Лекция 1: введение. Монады, отображения монад, дистрибутивные законы. Примеры: исключения, Читатель, Писатель, списки в ассортименте (в т. ч. непустые, свободные от повторений и т. п.), когда их действие можно переставлять.

Лекция 2: контейнеры, монадические контейнеры. Контейнер задаётся парой S: Set, P: S → Set. Интерпретация F=[|S, P|] контейнера действует в категорию [Set, Set] эндофункторов категории множеств по правилу: FX = {Ps → X}_{s: S}. Основной пример: список; S = Nat, Ps = [0, … s), FX = {[0, … s) → X} (список элементов типа X длины s это функция из [0, … s) в X). Основной результат: интерпретация является полным вложением (полным унивалентным функтором, fully faithful functor). Монадический контейнер это уже не пара, как обычный контейнер, а шестёрка. Интерпретация в этом случае является не просто функтором, а монадой.

Лекция 3: моноидальные функторы, комонады. Более естественное понятие направленного контейнера (5 ингридиентов) порождает комонады в качестве интерпретаций. Примеры направленных контейнеров: потоки (бесконечные коллекции, S = 1, P· = Nat), непустые списки.

Ссылки

• When is a container a comonad? — кроме прочего содержит хорошее введение в тему, как оно давалось на второй лекции. Основная тема статьи соответствует третьей лекции.

Встроенные предметно-ориентированные языки в Idris (Э. Брэди)

Лектор

Эдвин Брэди

Место работы: Университет Сэн Эндрюса, Шотландия.

Тема диссертации: Practical Implementation of a Dependently Typed Functional Programming Language, 2005, Durham U.

Основные публикации

• Inductive families need not store their indices, 2004, coauth. McBride, McKinna // Types for proofs and programs, pp. 115-129. Cit. 73.
• Idris, a general-purpose dependently typed programming language: Design and implementation, 2013 // Journal of Functional Programming 23 (05), pp. 552-593. Cit. 60.
• IDRIS---: systems programming meets full dependent types, 2011 // Proceedings of the 5th ACM workshop on Programming languages meets program verification, pp. 43-54. Cit. 51.

Недавние публикации

• Cross-platform Compilers for Functional Languages, 2015 // Under consideration for Trends in Functional Programming.
• Resource-Dependent Algebraic Effects, 2015 // Trends in Functional Programming, pp. 18-33.

Содержание

Лекция 1: знакомство с Idris. Idris это чистый функциональный язык с полноценными зависимыми типами. Синтаксис сильно похож на Haskell, реализация — на нём же. Компилируется в C, есть бэкенды JavaScript, Java и неоконченный LLVM, среди студенческих проектов упоминался в Erlang, демонстрировалась также компиляция в PHP. В отличие от Хаскеля семантика строгая, и вообще, делается упор на производительность (для этого во время компиляции много сил тратится на преобразования вроде стирания, erasure, и partial evaluation). Зависимые типы позволяют с высокой точностью сформулировать нужные свойства программы, а тайп-чекеру остаётся лишь проверить их. После компиляции получается «сертифицированная программа». Также большое внимание уделяется поддержке при составлении программы со стороны текстового редактора.

Лекция 2: EDSLs на Idris. Особое внимание при (продолжающемся) проектировании языка уделяется возможности реализации на нём предметно-ориентированных языков, с помощью которых можно было бы составлять (благодаря богатой системе зависимых типов Idris) сертифицированные программы для управления ресурсами, реализации сетевых проколов и т. п. Интересной особенностью Idris является Error Reflection, возможность добавлять собственные обработчики ошибок, что позволяет делать сообщения об ошибках в DSL более понятными пользователю, который может не понимать реализацию DSL. В ходе лекции приводились примеры спецификации и реализации протокола простого конечного автомата Дверь, сетевого протокола Echo, сетевого протокола для выполнения набора простых команд (умножение двух чисел, вычисления длины строки, возврата времени uptime). При реализации проколов существенно используются т. н. Uniqueness Types по аналогии с тем, как устроены одноимённые типы в языке Clean и ownership types в языке Rust.

Лекция 3: EDSLs с эффектами. Рассматривается проблема комбинирования эффектов на примере реализации интерпретатора простого языка выражений на Хаскеле с применением трансформеров монад. Пример переводится на Idris, где в EDSL Effects учитывается независимость отдельных эффектов и вводится простой синтаксис для перехода между разными эффектами в стеке.

Ссылки

• ГитХаб-аккаунт Э. Брэди — здесь можно найти репозитории со многими примерами, использованными на лекциях (хотя, порой в несколько изменённом виде).
• Конспект лекций.
• Эрланг-бэкенд для Idris, бакалаврская работа.

Эффективное в худшем случае обобщённое функциональное программирование с массивами данными (Ф. Хенглейн)

Лектор

Фриц Хенглейн

Место работы: Университет Копенгагена, Дания.

Тема диссертации: Polymorphic Type Inference and Semi-Unification, 1989, Rutgers U.

Основные публикации

• Type inference with polymorphic recursion, 1993 // ACM Transactions on Programming Languages and Systems 15 (2), pp. 253-289. Cit. 288.
• Dynamic typing: Syntax and proof theory, 1994 // Science of Computer Programming 22 (3), pp. 197-230. Cit. 168.
• Efficient type inference for higher-order binding-time analysis, 1991 // Functional Programming Languages and Computer Architecture, pp. 448-472. Cit. 153.

Недавние публикации

• Domain-specific languages for enterprise systems, 2014 // Leveraging Applications of Formal Methods, Verification and Validation, pp. 73-95.
• Optimally Streaming Greedy Regular Expression Parsing, 2014, coauth. Grathwohl, Rasmussen // Theoretical Aspects of Computing, pp. 224-240.

Содержание

Лекция 1: обобщённое дискриминирование. Широко известно, что сортировка, основанная на абстрактной функции сравнения, работает в лучшем случае за линеарифмическое время. В то же время существуют сортировки, учитывающие природу входных данных и работающие за линейное время. При этом, однако, речь вряд ли может идти об обобщённом программировании. В данной работе поставлена задача объединить сильные стороны этих двух групп сортировок. Предложены две ключевые идеи на этом пути. Первое это обобщение функции сортировки до так называемой дискриминирующей функции, частным случаем которой может быть решение не только задачи сортировки, но и, скажем, задача подсчёта количества уникальных элементов в коллекции. Второе это определение маленького DSL (или комбинаторной библиотеки) для определения отношения порядка в композиционном стиле. Всё в результате делается за линейное время почти для всех порядков, глубоко внутри всё равно лежит Bucket Sort. Реализация на некоторых задачах выигрывает у sortBy и qsort, хотя и использует нечистый unsafePerformIO.

Лекция 2: обобщённое программирование с мультимножествами. Рассматривается компактная Haskell-библиотека для реализации мультимножеств и операций над ними; интерфейс в основном ориентирован на представление операций, используемых в SQL. Считается, что благодаря ленивому (символическому) представлению таких асимптотически «неприятных» операций как декартово произведение можно получить более эффективную реализацию этого интерфейса. Принцип: откладывать выполнение квадратичных операций так долго, как возможно (при этом в некоторых случаях в конце концов они вообще оказываются не нужными). Операции типа INNER JOIN адаптируются под использование обобщённых дискриминаторов из первой лекции. Операции типа свёртки (максимум, подсчёт, сумма и т. п.) определяются с помощью анализа символической структуры рассматриваемого множества, по аналогии с тем, как дискриминаторы из первой лекции анализировали структуру заданного порядка.

Лекция 3: обобщённое программирование линейной алгебры. Мультимножества, рассмотренные на лекции 2, можно понимать как отображение a → Nat (обычные множества: a → Bool). Оказывается, что разработанные инструменты могут быть обобщены до отображений почти в любой числовой тип. Большая часть лекции посчёщена конструкциям из линейной алгебры, которые могут возникать при подобных обобщениях.

Темы первых двух лекций подробно описаны в двух статьях, ссылки на которые приведены ниже.

Ссылки

• Generic Top-down Discrimination for Sorting and Partitioning in Linear Time
• Generic Multiset Programming with Discrimination-based Joins and Symbolic Cartesian Products

Применение обобщенного программирования и программирования на уровне типов в Haskell (А. Лёх)

Лектор

Андрес Лёх

Место работы: компания Well-Typed.

Тема диссертации: Exploring Generic Haskell. 2004, Utrecht U.

Основные публикации

• Type-indexed data types, 2002, coauth. Hinze, Jeuring // Mathematics of Program Construction, pp. 148-174. Cit. 118.
• “Scrap Your Boilerplate” Reloaded, 2006, coauth. Hinze, Oliveira // Functional and Logic Programming, pp. 13-29. Cit. 77.
• Generic H∀ SKELL, Specifically, 2003, coauth. Clarke // Generic Programming, pp. 21-47. Cit. 76.

Недавние публикации

• The semantics of version control, 2014, coauth. Swierstra // Proceedings of the 2014 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software, pp. 43-54.
• Generic generic programming, 2014, coauth. Magalhaes // Practical Aspects of Declarative Languages, pp. 216-231.

Содержание

Обобщённое программирование в одном из смыслов можно трактовать как написание функций, относительно некоторого универсального представления «любого» типа данных; реальную конвертацию между типами и их представлениями можно осуществлять как вручную, так и автоматически по мере надобности. В терминах Хаскеля множество конвертируемых типов можно выразить как класс типов.

class Generic a where
	type Rep a
	from :: a -> Rep a
	to :: Rep a -> a

Универсальное представление может быть подсказано общим видом алгебраических типов данных, у которых имеется набор конструкторов значений, каждый конструктор принимает некоторое количество параметров. Такая структура хорошо отражается теоретико-множественной суммой произведений (sum of products), отсюда имя (ещё одной) библиотеки обобщённого программирования, основы которой были изложены на лекциях: generics-sop.

Для хранения произведений используется тип NP (n-ary product). Приведём пример значения этого типа.

(I (1::Int) :* I "Hi!" :* Nil) :: NP I '[Int, [Char]]

Первый аргумент NP (в данном случае I) служит для удобства: мы часто храним не просто списки типов (которые в данном случае реализуют теоретико-множественное произведение), а ещё и некий общий конструктор, который к ним применяется. В данном примере применяется тождественный конструктор (data I a = I a).

Сумма хранится аналогично, с помощью списка типов, но при этом конструктор значений чуть более сложен, чем :* выше, он позволяет указать, какой именно тип из списка был выбран.

type ExampleChoice = NS I ’[Char, Bool, Int]

c0, c1, c2 :: ExampleChoice
c0 = Z (I ’x’)
c1 = S (Z (I True))
c2 = S (S (Z (I 3)))

Приведём пример типа и его обобщённого представления на основе NS/NP.

data Expr =
	| NumL Int
	| BoolL Bool
	| Add Expr Expr
	| If Expr Expr Expr

type RepExpr = NS (NP I) (’ 
			[ ’[Int]
			, ’[Bool]
			, ’[Expr, Expr]
			, ’[Expr, Expr, Expr]
			])

«Простые» примеры, разобранные на лекциях: определение обобщённой функции сравнения на равенство, определение обобщённой константы «Значение по умолчанию».

Где можно применять обобщённое программирование:

• генерация тестовых данных,
• претти-принтинг,
• генерация JSON/XML-представлений.

Ссылки

• WGP 2014: Andres Löh — True Sums of Products — получасовой доклад, в котором излагается весь материал курса.
• Отличный конспект лекций, выданный лектором.

Типы данных типов данных (К. Макбрайд)

Лектор

Конор Макбрайд

Место работы: Университет Стрэтклайда, Шотландия.

Тема диссертации: Dependently Typed Functional Programs and theis Proofs, 1999, U. of Edinburg.

Основные публикации

• The view from the left, 2004, coauth. McKinna // Journal of Functional Programming 14 (1), pp. 69-111. Cit. 335.
• Applicative programming with effects, 2008, coauth. Paterson // Journal of functional programming 18 (01), pp. 1-13. Cit. 263.
• Faking it Simulating dependent types in Haskell, 2002 // Journal of functional programming 12 (4-5), pp. 375-392. Cit. 119.

Недавние публикации

• Indexed containers, 2015, coauth. Altenkirch, Ghani, Hancock, Morris // Journal of Functional Programming 25, e5.
• Hasochism: the pleasure and pain of dependently typed Haskell programming, 2014, coauth. Lindley // ACM SIGPLAN Notices 48 (12), pp. 81-92.

Содержание

Тематика курса пересекается с курсом Т. Уусталу и связана с семантикой контейнерных типов. Однако идёт дальше обычной категорной семантики, и предлагает так сказать механизированную семантику, а именно, обширную формализацию понятий нормального функтора (как бы «предконтейнера»), контейнера (как у Усталу) и, самое главное, индексированного контейнера на языке программирования Agda. Кроме определений Агда используется для формулировки свойств этих конструкций: замкнутости, траверсируемости, категорных свойств (определение морфизмов контейнеров и свободных монад на контейнерах). Апогей курса, достигнутый в конце последней лекции — определение универсального типа данных: data Data …, то есть с помощью встроенного средства языка (data) определяется объект (Data), который по своим возможностям не уступает исходному (data).

Ссылки

• Agda-листинг, который использовался в качестве слайдов на лекциях.
• Конспект, выданный до лекций — имеет ряд расхождений с лекциями (можно понять, если сравнивать с Agda-листингом из первой ссылки).

Метапрограммирование времени компиляции в информационном мире (Д. Сайм)

Лектор

Дон Сайм

Место работы: Microsoft Research в Кэмбридже, Великобритания.

Тема диссертации: ???, PhD studies in Cambridge U.

Основные публикации

• Design and implementation of generics for the .NET common language runtime, 2001, coauth. Kennedy // ACM SigPlan Notices 36 (5), pp. 1-12. Cit. 263.
• Proving Java type soundness, 1999 // Formal Syntax and Semantics of Java, 83-pp. 118. Cit. 161.
• Typing a multi-language intermediate code, 2001, coauth. Gordon // ACM SIGPLAN Notices 36 (3), pp. 248-260. Cit. 121.

Недавние публикации

• F# Data: Making structured data first class citizens, 2015, coauth. Petricek, Guerra // Unpublished draft.
• Expert F# 3.0, 2012, coauth. Granicz, A Cisternino // Apress.

Содержание

Укороченный курс (две лекции) посвящён важности технологии проводников типов (type provider) в языке F# и демонстрации её возможностей на ряде примеров (в том числе, сайта Международного банка). Данная технология позволяет решать проблему языков со строгой типизацией, которые не успевают меняться так же быстро, как источники данных, путём генерации типов для практически всех сущностей, которые найдены в инспектируемом источнике, на лету во время разработки. В качестве источников могут выступать web-страница, SQL-база данных, FTP-сервер и т. п.

Проводник типа состоит из

• библиотеки,
• адаптера между источником данных и системой типов .NET,
• плагин к компилятору/IDE.

В качестве IDE демонстрировалась Visual Studio, хотя утверждается, что в других окружениях тоже должно работать.

Ссылки

• Пособие по созданию проводника типов.
• Проводник типов для регулярного выражения.