- •Лекция 5. Ламбда-исчисление как формализация языка функционального программирования
- •5.2. Аксиомы ламбда-исчисления
- •5.2.1. Конвертируемость
- •6.1. Понятие комбинатора
- •6.2. Комбинаторная логика как формальная система
- •6.2.1. Правила конструирования допустимых для заданного алфавита комбинаторных выражений (термов).
- •6.2.2. Аксиомы комбинаторной логики
- •6.2.3.Умолчания
- •6.2.4. Синтаксис выражений комбинаторной логики
- •6.2.5. Редукция комбинаторных термов
- •6.2.6. Базис термов
- •7.1. Определение типов
- •7.2. Аксиомы вывода типа комбинатора
- •7.3. Типизация выражений в sml
- •7.3.1. Схема типизации
- •7.3.2. Выводимость типов
- •7.3.3. Полиморфная типизация
- •7.4. Преимущества типизации
- •7.5. Применение типизации
- •7.5.1. Статическая типизация
- •7.5.2. Полимофная типизация
- •7.6. Управление типами в технологии .Net
7.5.2. Полимофная типизация
Рассмотрим пример полиморфизма - оперирования функциями переменного типа.
Для иллюстрации исследуем поведение встроенной функции hd (от слова "head" - голова), которая выделяет "голову" (первый элемент) списка, вне зависимости от типа его элементов.
Пример 6. Применим функцию к списку из целочисленных элементов:
hd [1,2,3];
val it = 1 : int
Получим, что функция имеет тип функции из списка целочисленных величин в целое число (int list -> int).
Пример 7. В случае списка из значений истинности та же самая функция
hd [true, false, true, false];
val it = true: bool
возвращает значение истинности, т.е. имеет следующий тип:
bool list -> bool
Пример 8. Для случая списка кортежей из пар целых чисел
hd [(1,2)(3,4),(5,6)];
val it = (1,2) : int*int
получим тип:
((int*int)list -> (int*int)).
В итоге можно сделать вывод о том, что функция hd имеет тип (type list) -> type, где type - произвольный тип, т.е. полиморфна.
7.6. Управление типами в технологии .Net
Технологическая платформа .NET обеспечивает единообразное управление типами элементов всех языков программирования, реализованных на данной платформе. Это достигается за счет интегрированной обобщенной системы типизации, так называемой Common Type System, или, сокращенно, CTS.
Основная особенность CTS заключается в том, что она представляет собой единую иерархию типов, и типы объектов программы, написанной на произвольном языке программирования, который поддерживается технологической платформой .NET, в ходе трансляции автоматически преобразуются в соответствующие им типы Common Type System.
Таким образом, для любого языка программирования существует отображение (функция), преобразующая произвольный тип этого языка в тот или иной тип Common Type System. Естественно, язык программирования SML не является исключением. Приведем в подтверждение фрагмент отображения типов языка программирования SML в типы иерархии CTS, оформив это соответствие в виде таблицы 7.1.
Таблица 7.1. Отображение типов языка программирования SML в типы иерархии CTS
№ |
Тип |
Класс.NET |
Пояснение |
1 |
int |
System.Int32 |
Целое число |
2 |
string |
System.String |
Строка |
3 |
bool |
System.Boolean |
Логическое значение |
... |
... |
... |
... |
Позднее мы обсудим подобное соответствие типов для языка программирования C#.
Иерархия типов в .NET
Рассмотрим более подробно обобщенную систему типизации, принятую в .NET.
Как явствует из схемы, Common Type System представляет собой иерархию, в которой стрелки указывают в сторону уменьшения общности типа.
Типы иерархии CTS подразделяются на ссылочные типы (pointer type) и типы-значения (value type).
Особенностями ссылочных типов являются необходимость использования указателей на типизированные объекты, а также централизованное хранение и освобождение памяти ("сборка мусора").
Одной из характеристик типов-значений является то обстоятельство, что они не участвуют в наследовании. Кроме того, типы-значения копируются при присваивании значения.
В свою очередь, ссылочные типы могут принимать одну из трех форм:
объектные типы (object type);
интерфейсные типы (interface type);
типы указателей (pointer type).
В случае отсутствия стандартного типа нужной формы, пользователь имеет возможность конструировать собственный тип, который может быть как ссылочным типом, так и типом-значением.
Система CTS обеспечивает безопасную типизацию, т.е. гарантирует отсутствие побочных эффектов (переполнение оперативной памяти компьютера, некорректное преобразование типов и т.д.).
Выводы по лекции 7
Подводя итоги рассмотрения основных аспектов теории типов и типизации в языках программирования, можно сделать следующие выводы.
1. Теории с типами и языки программирования с типизацией имеют значительно более высокую вычислительную мощность, а, следовательно, более высокую теоретическую и прикладную значимость.
2. Технологическая платформа .NET обеспечивает ряд несомненных дополнительных преимуществ перед другими известными платформами в отношении системы типов:
- технология .NET использует централизованную, унифицированную, интегрированную систему типизации Common Type System (CTS), общую для всех языков программирования, реализуемых на данной платформе.
- в рамках технологической платформы .NET обеспечивается строгое, однозначное соответствие между примитивными типами языков программирования и базовыми классами .NET. Большинство компиляторов для языков программирования, которые реализованы для платформы .NET, имеют встроенную поддержку примитивных типов.
3. Целям безопасности типизации служит явное разделение на ссылочные типы и типы-значения, а также гибкий и надежный механизм преобразования типов-значений в ссылочные (известный под названием boxing) и обратно (известный под названием unboxing).
Для более подробного самостоятельного ознакомления с тематикой лекции рекомендуется следующий список источников: [32, 43, 44, 59].
