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

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

Лектор

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

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

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