Типы в языках программирования — Эта книга, уже давно ставшая классической, содержит всестороннее введение в системы типов, применяемые в информатике. Среди рассматриваемых тем - нетипизированное лямбда-исчисление, простые системы типов, полиморфизм, вложение типов и рекурсивные типы. Каждая из рассматриваемых концепций сопровождается множеством примеров и задач, что позволяет закрепить теоретический материал. Книга будет полезна как для практикующих разработчиков, так и для студентов и аспирантов в области информатики.
Название: Типы в языках программирования Автор: Бенджамин Пирс Издательство: Лямбда пресс, Добросвет Год: 2010 Страниц: 656 Формат: PDF Размер: 5,43 Мб Качество: Отличное Язык: Русский
Содержание:
Предисловие 1. Введение 1.1. Типы в информатике 1.2. Для чего годятся типы 1.3. Системы типов и проектирование языков 1.4. Краткая история 1.5. Дополнительная литература 2. Математический аппарат 2.1. Множества, отношения и функции 2.2. Упорядоченные множества 2.3. Последовательности 2.4. Индукция 2.5. Справочная литература I Бестиповые системы 3. Бестиповые арифметические выражения 3.1. Введение 3.2. Синтаксис 3.3. Индукция на термах 3.4. Семантические стили 3.5. Вычисление 3.6. Дополнительные замечания 4. Реализация арифметических выражений на языке ML 4.1. Синтаксис 4.2. Вычисление 4.3. Что осталось за кадром 5. Бестиповое лямбда-исчисление 5.1. Основы 5.2. Программирование на языке лямбда-исчисления 5.3. Формальности 5.4. Дополнительные замечания 6. Представление термов без использования имен 6.1. Термы и контексты 6.2. Сдвиг и подстановка 6.3. Вычисление 7. Реализация лямбда-исчисления на ML 7.1. Термы и контексты 7.2. Сдвиг и подстановка 7.3. Вычисление 7.4. Дополнительные замечания II Простые типы 8. Типизированные арифметические выражения 8.1. Типы 8.2. Отношение типизации 8.3. Безопасность = продвижение + сохранение 9. Простое типизированное лямбда-исчисление 9.1. Типы функций 9.2. Отношение типизации 9.3. Свойства типизации 9.4. Соотношение Карри-Говарда 9.5. Стирание типов и типизируемость 9.6. Стиль Карри и стиль Чёрча 9.7. Дополнительные замечания 10. Реализация простых типов на ML 10.1. Контексты 10.2. Термы и типы 10.3. Проверка типов 11. Простые расширения 11.1. Базовые типы 11.2. Единичный тип 11.3. Производные формы: последовательное исполнение и связывания-пустышки 11.4. Приписывание типа 11.5. Связывание let 11.6. Пары 11.7. Кортежи 11.8. Записи 11.9. Типы-суммы 11.10. Варианты 11.11. Рекурсия общего вида 11.12. Списки 12. Нормализация 12.1. Нормализация для простых типов 12.2. Дополнительные замечания 13. Ссылки 13.1. Введение 13.2. Типизация 13.3. Вычисление 13.4. Типизация содержимого памяти 13.5. Безопасность 13.6. Дополнительные замечания 14. Исключения 14.1. Порождение исключений 14.2. Обработка исключений 14.3. Исключения, сопровождаемые значениями III Подтипы 15. Подтипы 15.1. Включение 15.2. Отношение подтипирования 15.3. Свойства подтипов и типизации 15.4. Типы Тор и Bottom 15.5. Подтипы и другие элементы языка 15.6. Семантика подтипов, основанная на преобразованиях типов 15.7. Типы-пересечения и типы-объединения 15.8. Дополнительные замечания 16. Метатеория подтипов 16.1. Алгоритмическое отношение подтипирования 16.2. Алгоритмическое отношение типизации 16.3. Пересечения и объединения 16.4. Алгоритмическая типизация и тип Bot 17. Реализация подтипов на ML 17.1. Синтаксис 17.2. Подтипы 17.3. Типизация 18. Расширенный пример: императивные объекты 18.1. Что такое объектно-ориентированное программирование? 18.2. Объекты 18.3. Генераторы объектов 18.4. Подтипы 18.5. Группировка переменных экземпляра 18.6. Простые классы 18.7. Добавление новых переменных экземпляра 18.8. Вызов методов надкласса 18.9. Классы с переменной self 18.10. Открытая рекурсия через self 18.11. Открытая рекурсия и порядок вычислений 18.12. Более эффективная реализация 18.13. Резюме 18.14. Дополнительные замечания 19. Расширенный пример: Облегченная Java 19.1. Введение 19.2. Обзор 19.3. Именные и структурные системы типов 19.4. Определения 19.5. Свойства 19.6. Объекты: кодирование или элементарное понятие? 19.7. Дополнительные замечания IV Рекурсивные типы 20. Рекурсивные типы 20.1. Примеры 20.2. Формальные определения 20.3. Подтипы 20.4. Дополнительные замечания 21. Метатеория рекурсивных типов 21.1. Индукция и коиндукция 21.2. Конечные и бесконечные типы 21.3. Подтипы 21.4. Отступление о транзитивности 21.5. Проверка принадлежности 21.6. Более эффективные алгоритмы 21.7. Регулярные деревья 21.8. ц-типы 21.9. Подсчет подвыражений 21.10. Отступление: экспоненциальный алгоритм 21.11. Подтипирование для изорекурсивных типов 21.12. Дополнительные замечания V Полиморфизм 22. Реконструкция типов 22.1. Типовые переменные и подстановки 22.2. Две точки зрения на типовые переменные 22.3. Типизация на основе ограничений 22.4. Унификация 22.5. Главные типы 22.6. Неявные аннотации типов 22.7. Полиморфизм через let 22.8. Дополнительные замечания 23. Универсальные типы 23.1. Мотивация 23.2. Разновидности полиморфизма 23.3. Система F 23.4. Примеры 23.5. Основные свойства 23.6. Стирание, типизируемость и реконструкция типов 23.7. Стирание и порядок вычислений 23.8. Варианты Системы F 23.9. Параметричность 23.10. Импредикативность 23.11. Дополнительные замечания 24. Экзистенциальные типы 24.1. Мотивация 24.2. Абстракция данных при помощи экзистенциальных типов 24.3. Кодирование экзистенциальных типов 24.4. Дополнительные замечания 25. Реализация Системы F на ML 25.1. Представление типов без использования имен 25.2. Сдвиг типов и подстановка 25.3. Термы 25.4. Вычисление 25.5. Типизация 26. Ограниченная квантификация 26.1. Мотивация 26.2. Определения 26.3. Примеры 26.4. Безопасность 26.5. Ограниченные экзистенциальные типы 26.6. Дополнительные замечания 27. Расширенный пример: еще раз императивные объекты 28. Метатеория ограниченной квантификации 28.1. Выявление 28.2. Минимальная типизация 28.3. Подтипы в ядерной F<: 28.4. Подтипы в полной F<: 28.5. Неразрешимость полной F<; 28.6. Объединения и пересечения 28.7. Ограниченные кванторы существования 28.8. Ограниченная квантификация и тип Bot VI Системы высших порядков 29. Операторы над типами и виды 29.1. Неформальное введение 29.2. Определения 30. Полиморфизм высших порядков 30.1. Определения 30.2. Пример 30.3. Свойства исчисления 30.4. Варианты Fw 30.5. Идем дальше: зависимые типы 31. Подтипы высших порядков 31.1. Интуитивные понятия 31.2. Определения 31.3. Свойства исчисления 31.4. Дополнительные замечания 32. Расширенный пример: чисто функциональные объекты 32.1. Простые объекты 32.2. Подтипы 32.3. Ограниченная квантификация 32.4. Типы интерфейсов 32.5. Отправка сообщений объектам 32.6. Простые классы 32.7. Полиморфные обновления 32.8. Добавление переменных экземпляра 32.9. Классы с переменной self 32.10Дополнительные замечания Приложения А. Решения избранных упражнений В. Принятые обозначения В. Имена метапеременных В. Имена правил В. Соглашения по именам и индексам Литература Список иллюстраций Предметный указатель
