Летняя школа в г.Оксфорд 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), непустые списки.

Встроенные предметно-ориентированные языки в 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 учитывается независимость отдельных эффектов и вводится простой синтаксис для перехода между разными эффектами в стеке.

Ссылки

• ГитХаб-аккаунт Э. Брэди.

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

Лектор

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

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

Тема диссертации: 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.

Применение обобщенного программирования и программирования на уровне типов в 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.

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

Лектор

Дон Сайм

Место работы: 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.

Содержание

Ссылки

• Regex TypeProvider