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

Материал из Вики ИТ мехмата ЮФУ
Перейти к: навигация, поиск
(→‎Содержание)
(→‎Содержание: Лёх)
Строка 103: Строка 103:
 
* Generic generic programming, 2014, coauth. Magalhaes // ''Practical Aspects of Declarative Languages'', pp. 216-231.
 
* 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), отсюда имя (ещё одной) библиотеки обобщённого программирования, основы которой были изложены на лекциях: [https://hackage.haskell.org/package/generics-sop 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-представлений.
  
  

Версия 19:43, 16 июля 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-представлений.


Ссылки

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

Лектор

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

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

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

Содержание

Источник — «http://it.mmcs.sfedu.ru/_wiki/index.php?title=Летняя_школа_в_г.Оксфорд_2015&oldid=6052»