Важнейшие работы в области типизации 1960-е – Р. Хиндли (Roger Hindley) исследовал типизацию в комбинаторной логике для моделирования языков функционального. - презентация

1

2

3 Важнейшие работы в области типизации 1960-е – Р. Хиндли (Roger Hindley) исследовал типизацию в комбинаторной логике для моделирования языков функционального программирования со строгой типизацией 1969 – Р. Хиндли исследовал полиморфные системы типов 1978 – Р. Милнер (Robin Milner) предложил расширенную систему полиморфной типизации для ML Современные языки программирования и.NET: II семестр Лекция 6: Теория типов и типизация в.NET © Учебный Центр безопасности информационных технологий Microsoft Московского инженерно-физического института (государственного университета), 2003

4 Современные языки программирования и.NET: II семестр Лекция 6: Теория типов и типизация в.NET © Учебный Центр безопасности информационных технологий Microsoft Московского инженерно-физического института (государственного университета), 2003 Общие сведения о типизации Тип (сорт) – относительно устойчивая и независимая совокупность элементов, которую можно выделить во всем рассматриваемом множестве (предметной области). Задать тип T (как и любое множество) возможно: 1)явным перечислением элементов; 2)формализацией общих свойств элементов предметной области d D посредством индивидуализирующей предикатной функции, значение которой истинно, если элемент принадлежит данному типу и ложно в противном случае: T = {d: D| }

5 Современные языки программирования и.NET: II семестр Лекция 6: Теория типов и типизация в.NET © Учебный Центр безопасности информационных технологий Microsoft Московского инженерно-физического института (государственного университета), 2003 Типы в математике (1) Чистой системой типов называется семейство ламбда- исчислений, в которых каждый элемент характеризуется тройкой, где: S – подмножество констант, называемых сортами; A – множество аксиом вида c:s, где с-константа, s-сорт; R – множество троек сортов, определяющих возможные функциональные пространства и их сорта для системы Приписывание ламбда-терму M типа T обозначим как #M | T (читается: «ламбда-терм M имеет тип T»)

6 Современные языки программирования и.NET: II семестр Лекция 6: Теория типов и типизация в.NET © Учебный Центр безопасности информационных технологий Microsoft Московского инженерно-физического института (государственного университета), 2003 Типы в математике (2) Система типов формируется следующим образом: 1)задается множество базисных типов 1, 2, …; 2)всякий базисный тип считается типом; 3)если a и b считаются типами, то функция из a в b считается типом и имеет тип a b. В основе теории типов лежит принцип иерархичности: производные типы содержат базисные как подмножества. Это справедливо и для языков программирования (аналогично строятся иерархии классов в ООП).

7 Современные языки программирования и.NET: II семестр Лекция 6: Теория типов и типизация в.NET © Учебный Центр безопасности информационных технологий Microsoft Московского инженерно-физического института (государственного университета), 2003 Преимущества типизации Модель предметной области лучше структурирована, существует иерархия сортов элементов Манипулирование элементами более целенаправленно, разнородные элементы обрабатываются различным образом, однородные - единообразно В случае строгой типизации несоответствия типов фиксируются до выполнения программы, гарантируя отсутствие смысловых ошибок и безопасность кода

8

9 Современные языки программирования и.NET: II семестр Лекция 6: Теория типов и типизация в.NET © Учебный Центр безопасности информационных технологий Microsoft Московского инженерно-физического института (государственного университета), 2003 Иерархия типов в.NET Общая система типов Common Type System (CTS) Типы-значенияСсылочные типы Встроенные типы-значения Объект- ные типы Интерфейс- ные типы Типы указателей Типы-значения и ссылочные типы, заданные пользователем

10 Управление типами в CTS Типы могут использоваться после инициализации (с учетом метода вызова, свойств get и set и т.д.) Над типами могут совершаться преобразования (как явным, так и неявным образом) Типы объединяются в совокупности (пространства имен, файлы, сборки) Важнейшими подкатегориями системы типизации в.NET являются ссылочные типы (reference type) и типы-значения (value type) Современные языки программирования и.NET: II семестр Лекция 6: Теория типов и типизация в.NET © Учебный Центр безопасности информационных технологий Microsoft Московского инженерно-физического института (государственного университета), 2003

11 Ссылочные типы и типы-значения в.NET и C# (1) Типы-значения: –непосредственно содержат объекты данных; –не могут быть пустыми (null) Ссылочные типы: –содержат ссылки на объекты данных; –могут быть пустыми (null) Пример: int i = 25; string s = John_Smith"; 25 i s "John_Smith" Современные языки программирования и.NET: II семестр Лекция 6: Теория типов и типизация в.NET © Учебный Центр безопасности информационных технологий Microsoft Московского инженерно-физического института (государственного университета), 2003

12 Ссылочные типы и типы-значения в.NET и C# (2) Типы-значения : –элементарные: int i; float x; –перечислимые: enum State { Off, On } –структурные: struct Point {int x,y;} Ссылочные типы : –корневые: object –строковые: string –классы: class Foo: Bar, IFoo {...} –интерфейсы: interface IFoo: IBar {...} –массивы: string[] a = new string[10]; –делегаты: delegate void Empty(); Современные языки программирования и.NET: II семестр Лекция 6: Теория типов и типизация в.NET © Учебный Центр безопасности информационных технологий Microsoft Московского инженерно-физического института (государственного университета), 2003

13 Типы-значенияСсылочные типы Переменная содержит значениессылку на значение Переменная хранится в стекев куче Значение по умолчанию 0, false, '\0'null Оператор присваивания копирует значениекопирует ссылку Пример int i = 25;string s = John"; int j = i;string s1 = s; Сопоставление ссылочных типов и типов-значений 25 i j s s1 J o h n Современные языки программирования и.NET: II семестр Лекция 6: Теория типов и типизация в.NET © Учебный Центр безопасности информационных технологий Microsoft Московского инженерно-физического института (государственного университета), 2003

14 Элементарные типы языка С# (в сопоставлении с языком SML) C# CTS SMLДиапазон sbyteSystem.SByte byteSystem.Byte byte shortSystem.Int16 int ushortSystem.UInt16 word longSystem.Int floatSystem.Single real 1.5E E38 (32 Bit) doubleSystem.Double --- 5E E308 (64 Bit) decimalSystem.Decimal --- 1E E28 (128 Bit) boolSystem.Boolean booltrue, false charSystem.Char charСимвол (в коде unicode) Современные языки программирования и.NET: II семестр Лекция 6: Теория типов и типизация в.NET © Учебный Центр безопасности информационных технологий Microsoft Московского инженерно-физического института (государственного университета), 2003

15

16 Соглашения о преобразовании типов в.NET Неявные преобразования (происходят автоматически, всегда успешно завершаются, без потери точности) Явные преобразования (требуют вызова, могут завершаться ошибкой, а также приводить к потере точности) Оба типа преобразований могут быть инициированы пользователем int x = 25; long y = x; // неявное short z = (short)x;// явное double d = ; float f = (float)d;// явное long l = (long)d;// явное Современные языки программирования и.NET: II семестр Лекция 6: Теория типов и типизация в.NET © Учебный Центр безопасности информационных технологий Microsoft Московского инженерно-физического института (государственного университета), 2003

17 Пространства имен в.NET (1) Пространство имен (namespace) предоставляет средства уникальной идентификации типа Дает возможность логически структурировать систему типов Пространства имен могут объединять сборки Пространства имен могут быть вложенными Между пространствами имен и файлами нет однозначного соответствия Полное имя типа содержит все пространства имен Современные языки программирования и.NET: II семестр Лекция 6: Теория типов и типизация в.NET © Учебный Центр безопасности информационных технологий Microsoft Московского инженерно-физического института (государственного университета), 2003

18 Пространства имен в.NET (2) Пример описания пространств имен (в комментариях приведены полные имена): namespace N1 { // N1 class C1 { // N1.C1 class C2 { // N1.C1.C2 } namespace N2 { // N1.N2 class C2 {// N1.N2.C2 } Современные языки программирования и.NET: II семестр Лекция 6: Теория типов и типизация в.NET © Учебный Центр безопасности информационных технологий Microsoft Московского инженерно-физического института (государственного университета), 2003

19 Пространства имен в.NET (3) Оператор using : позволяет использовать типы без указания полного имени; может использоваться с полным именем; также используется для указания альтернативных имен (alias). using N1; C1 a;// Имя N1. является неявным N1.C1 b;// Полное имя C2 c;// Ошибка: имя C2 не определено N1.N2.C2 d;// Один из (под)классов C2 C1.C2 e;// Еще один из (под)классов C2 using C1 = N1.N2.C1; using N2 = N1.N2; C1 a;// Соответствует имени N1.N2.C1 N2.C1 b;// Соответствует имени N1.N2.C1 Современные языки программирования и.NET: II семестр Лекция 6: Теория типов и типизация в.NET © Учебный Центр безопасности информационных технологий Microsoft Московского инженерно-физического института (государственного университета), 2003

20 Пространства имен и ссылки В Visual Studio для проекта могут быть указаны ссылки Каждая ссылка идентифицирует уникальную сборку Передается C# компилятору по ссылке ( /r или /reference ) csc HelloWorld.cs /reference:System.WinForms.dll Пространства имен дают возможность сокращенного именования на уровне языка программирования –(устраняют необходимость многократного повторения полного имени) Ссылки указывают на сборку для использования в проекте Современные языки программирования и.NET: II семестр Лекция 6: Теория типов и типизация в.NET © Учебный Центр безопасности информационных технологий Microsoft Московского инженерно-физического института (государственного университета), 2003

21 Современные языки программирования и.NET: II семестр Лекция 6: Теория типов и типизация в.NET © Учебный Центр безопасности информационных технологий Microsoft Московского инженерно-физического института (государственного университета), 2003 Преимущества типизации на платформе.NET 1.Использование централизованной, унифицированной системы типизации Common Type System (CTS) 2.Строгое соответствие между примитивными типами языков программирования и базовыми классами.NET; встроенная поддержка примитивных типов большинством компиляторов для.NET 3.Явное разделение на ссылочные типы (используются через указатель; централизованно хранятся и освобождаются) и типы-значения (не участвуют в наследовании; при присваивании значения копируются) 4.Гибкий и надежный механизм преобразования типов- значений в ссылочные (boxing) и обратно (unboxing)

22 Современные языки программирования и.NET: II семестр Лекция 6: Теория типов и типизация в.NET © Учебный Центр безопасности информационных технологий Microsoft Московского инженерно-физического института (государственного университета), 2003 Библиография 1.Curry H.B., Feys R. Combinatory logic, vol.I, North Holland, Amsterdam, Hindley J.R., Seldin J.P. Introduction to combinators and - calculus. London Mathematical Society Student Texts, 1, Cambridge University Press, Milner R. A theory of type polymorphism in programming languages. Journal of Computer and System Science, 17(3): , Hindley J.R. The principal type-scheme of an object in combinatory logic. Trans. Amer. Math. Soc., 146:29-60, 1969