Введение в ФП :-\
Andrei Melnikov
Литература для подготовки:
"Плазмеер" - Functional Programming and Parallel Graph Rewriting
(1993) by Rinus Plasmeijer
http://clean.cs.ru.nl/contents/Addison__Wesley_book/addison__wesley_book.html
"Барендрегт" - Lambda Calculi with Types (1992) by by Henk Barendregt
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.4391
"Карделли" - On understanding types, data abstraction, and
polymorphism (1985) by Luca Cardelli
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.117.695
Материала там очень много, никакой речи о том, чтобы вы прочитали это
всё, не идёт. Прочитайте то, что соответствует плану доклада, и потом
на встрече в процессе обсудим.
Итак наброски плана.
Я планирую не сильно углубляться в теорию, т.е. по стилю это будет
скорее Карделли с Плазмеером, нежели Барендрегт.
1. Математические модели вычислений в ЯП
1.1. ЛИ (нетипизированное): синтаксис, подстановка как модель
вычисления, правила редукции
1.2. Нормальная форма, Чёрч-Россеровость, стратегии редукции,
строгость, needed redex
1.3. TRS как способ моделировать pattern matching
1.4. GRS как способ моделировать sharing
2. Математические модели систем типов в ЯП
2.1. Исторический обзор типов в ЯП
2.2. Явная и неявная типизация (по Чёрчу и Карри)
2.3. Simply Typed Lambda Calculus
2.4. Polymorphic Lambda Calculus (он же лямбда-2 и system F)
3. Краткий обзор продвинутых систем типов. Что интересного позволяет
делать каждая из систем типов, без детального рассмотрения систем.
Чтобы было понятно, какие системы вообще существуют.
3.1. "мейнстримовые" расширения: intersection types, bounded
polymorphism, existential types, sum/production types, лямбда-омега
3.2. лямбда-С и родственные системы
3.3. Ресурсные типы и родственные системам типов техники (линейные,
ownership types, region inference/static reference counting, abstract
interpretation/abstract reduction, strictness analysis)
Получилось огого материала, но в такой последовательности получится
снизить минимальный требуемый для понимания уровень знаний. Получается
надо минимум три доклада :-(
А ещё хорошо бы сделать "пункт 0". Введение в современную
(мета)математику
(Аристотель-Кант-Кантор-Фреге-Рассел-Чёрч-Карри-Клини-Мартин-Лёф), и
ответвление от него, посвящённое роли систем типов в формализации
математики, некий исторический обзор, параллельный моему 2.1. Но это
снова целый учебный курс.
Есть у кого соображения как это всё разгрести? Поделить, сократить?
Андрей
Oleg Smirnov
On May 15, 4:15 am, Andrei Melnikov <andy.melni...@gmail.com> wrote:
> А ещё хорошо бы сделать "пункт 0". Введение в современную
> (мета)математику
> (Аристотель-Кант-Кантор-Фреге-Рассел-Чёрч-Карри-Клини-Мартин-Лёф), и
> ответвление от него, посвящённое роли систем типов в формализации
> математики, некий исторический обзор, параллельный моему 2.1. Но это
> снова целый учебный курс.
>
> Есть у кого соображения как это всё разгрести? Поделить, сократить?
Пункт 0 можно начать изучать по лекциям Рассела. К списку я бы еще
добавил Карнапа и Витгенштейна.
Вопрос только будет ли кому-то это интересно? Лекции будут слегка
далеки от практики.
--
Regards,
Oleg Smirnov
Andrei Melnikov
бы хотели услышать, что можно опустить, в каком порядке излагать и т
п.
Что касается практичности пункта 0, на встрече я говорил о том, что
далекие от практики разделы изучать не нужно. Возьмём, скажем,
практикующего хаскеллиста. Он апгрейдится до GHC 6.10, читает в README
что добавили type families, ищет информацию по type families и находит
документ с такой прекрасной аннотацией:
Type Invariants for Haskell
Multi-parameter type classes, functional dependencies, and recently
GADTs and open type families open up opportunities to use complex
type-level programming to let GHC’s type checker verify various
properties of your programs.
Документ весьма практический, даже примеры кода кругом, а не странные
значки и горизонтальные линии, как у Барендрегта. Читает он читает, а
там между примерами пассажи вроде этого:
While type family instances are really the programmer-provided axioms
of type families, invariants should be derivable from those axioms. An
invariant which is not derivable is not a proper invariant, and may
introduce unsoundness.
Для понимания этого фрагмента программист должен знать, что такое:
- axiom
- derivable
- soundness
И почему unsoundness - это плохо.
Что в свою очередь требует знаний формальных систем и мат. логики, что
в свою очередь требует знаний основ теории моделей и теории
доказательств. Ну и так далее.
Знание того, в каких теориях множеств существуют недоступные
кардиналы, для понимания компьютерной литературы, мягко говоря, не
очень важно. Т.е. курс должен и может быть построен, исходя из
практических потребностей. Возьмите к примеру учебник по анализу для
технических вузов Фихтенгольца. Для понимания анализа необходимы
теория чисел и теория множеств. Но излагаются лишь какие-то маленькие
фрагментики этих теорий, и то на пальцах. Так же должно быть и у нас -
постепенное углубление имеющихся математических знаний, а не
последовательное изложение оснований математики. В таком виде курс
будет интересен всем, кто читает околохаскельные научные работы, а
таких, судя по встрече, много.