Сошников Дмитрий Валерьевич к.ф.-м.н., доцент dmitryso@microsoft.com Факультет инноваций и высоких технологий Московский физико-технический институт. - презентация

1 Сошников Дмитрий Валерьевич к.ф.-м.н., доцент Факультет инноваций и высоких технологий Московский физико-технический институт

2 2 Лекция 21 Типизация в языках функционального программирования

3 ©2008 Сошников Д.В. 3 Компиляторам с императивных языков программирования надо было знать, сколько памяти отводить под переменную Тип = объем памяти + способ интерпретации по умолчанию (signed/unsigned) В теории: Множество значений Множество операций и отношений

4 ©2008 Сошников Д.В. 4 Встроенные типы Конструируемые (получаемые из встроенных) типы Перечислимый, диапазон Указатели Функциональные типы Способы комбинирования типов: Массивы, записи, файлы Абстрактные типы данных Функциональность типа данных, реализованная как набор процедур/функций, удовлетворяющих заданным аксиомам

5 ©2008 Сошников Д.В. 5 Память выделяется (и освобождается) динамически нет необходимости знать размер объекта заранее Система типов (если есть) помогает контролировать семантическую правильность программы Может ли выражение быть применено к аргументу Более эффективная работа программы на этапе выполнения Нет необходимости хранить информацию о типах

6 ©2008 Сошников Д.В. 6 Проверяется строгое соответствие типов Возможные исключения: наследование, полиморфизм Pascal, F#, C#, Java, SML, … Языки со строгой типизацией Тип данных в основном нужен для определения объема памяти Совместимые по природе объекты (указатели на разные типы) совместимы по присваиванию С, С++ Языки с нестрогой типизацией Переменные могут принимать значения различной природы LISP, Prolog, … Бестиповые языки (динамические)

7 ©2008 Сошников Д.В. 7 Статический контроль типов На этапе компиляции Позволяет устранять большинство логических ошибок до запуска программы Более эффективная программа, поскольку упоминание типов в откомпилированной программе отсутствует Требует более жесткой системы типизации В традиционных языках обычно требует избыточного описания типов в программе Динамический контроль типов Происходит на этапе выполнения Меньше возможностей обнаружить ошибку Может быть смоделирован на бестиповых языках Более гибкий

8 ©2008 Сошников Д.В. 8 Системы типов в функциональных языках базируются на строгих математических формализмах Типизированное λ-исчисление Распространен автоматический вывод типов Программисту не нужно указывать тип значений => существнно более компактная запись! Широко используется полиморфизм и параметрическая типизация (generics) можно один раз определить операцию сразу для целого класса типов

9 ©2008 Сошников Д.В. 9 ТипСинтаксис F# Базовые типы: bool, int, char, string, …type t = int Функциональный тип T1 T2type t = T1->T2 Декартово произведение T1 T2 type t = T1*T2 Прямая (помеченная) суммаT1 + T2type t = Op1 of T1 | Op2 of T2 Мономорфные типы Полиморфные типы type a list = nil | cons of a*a list type a list = [] | a::a list

10 ©2008 Сошников Д.В. 10 T1+T2 – множество значений Т1 Т2, при этом можно различать между тем, какого типа конкретное значение T=T1+T2+…+T n = { | i 1..n, x i T i } isT i : T bool makeT i : T i T

11 ©2008 Сошников Д.В. 11 Приписывание типа выражению: x: Синтаксис: ::= : | ( ) | | λ :. | (e 1 e 2 ):, если e 1 :, e 2 : (λx:.e):, если e: Пример недопустимого выражения: (λx:. x x) Проверка vs. вывод типов: let f = fun x:int -> x in f 3 let f = fun x->x in f 3

12 ©2008 Сошников Д.В. 12 Система вывода типов должна уметь находить наиболее общий тип для выражения (либо приходить к противоречию) hd: a list a При проверке возможности применения выражений требуется совместимость типов, т.е. необходимо найти подстановку переменных типов hd [1;2;3] : (a list a) int list = int (a = int) Для сложной программы это приводит к необходимости рассматривать уравнения на типах

13 ©2008 Сошников Д.В. 13 let f x = x in f 3 τ 3 = int – базовый тип τ f = int ρ 1 – применение f 3 τ x = ρ 2 – тип x неизвестен τ f = ρ 2 ρ 3 – применение f x ρ 2 = ρ 3 – равные типы у двух частей равенства Решение системы уравнений: ρ 1 = ρ 2 = ρ 3 = int Это означает правильность выражения с точки зрения теории типов

14 ©2008 Сошников Д.В. 14 τ null = list τ 1 bool τ nil = list τ 2 τ hd = list τ 3 τ 3 τ tl = list τ 4 list τ 4 τ cons = τ 5 × list τ 5 τ 5 let map f m = if null m then nil else cons(f(hd m),map f tl(m)) τ m = list τ 1 τ (hd m) = τ 1 τ (tl m) = list τ 1 τ f = τ 1 τ 6 τ f(hd m) = τ 6 τ cons(f(hd m),map f tl(m)) = τ 6 τ map f tl(m) = τ 6 τ map = (τ 1 τ 6 ) list τ 1 list τ 6

15 ©2008 Сошников Д.В. 15 g =λf.(f 3, f true) τ f = int τ 1 τ f = bool τ 1 let f = λx.x in (f 3, f true) τ f = τ 1 τ 1 τ f1 = int τ 2 = int int τ f2 = bool τ 3 = bool bool

16 ©2008 Сошников Д.В. 16 Генерация уравнений A={x 1 :τ 1, …} – множество допущений τ(A,t) – тип выражения t при допущениях A τ(A,t) = σ, если t:σ A τ(A,f x) = σ, если τ(A,f) = σ, τ(A,x) = τ(A,λx:σ.e) = σ τ(A {x:σ},e) Пример: (λf.f 3)(λx.x) τ(A, 3) = int τ(A, f) = ρ 0 ρ 1 τ(A, f 3) = ρ 1 ; ρ 0 =int τ(A, λf.f 3) = (ρ 0 ρ 1 ) ρ 1 τ(A, λx.x) = ρ 3 ρ 3 τ(A, (λf.f 3)(λx.x)) - ? ( ρ 3 ρ 3 ) = ( ρ 0 ρ 1 )

17 ©2008 Сошников Д.В. 17 Унификация типовых переменных u({e 1,…,e n }) = : T var T u(( =T) E) = u(E) ( T) u(( = ) E) = u({( = ),( = )} E) Пример u({(ρ 3 ρ 3 )=(ρ 0 ρ 1 ), ρ 0 =int}) = u({ρ 3 =ρ 0,ρ 3 =ρ 1, ρ 0 =int})

18 ©2008 Сошников Д.В. 18 Формальная аксиоматическая система Допущения (assertions): x : τ Выводы: A x : τ A={x 1 :τ 1, …} – множество допущений Правила вывода: Аксиома: A {x : τ} x : τ А (Name) B

19 ©2008 Сошников Д.В. 19 А c:bool; А a:τ; А b:τ (Cond) A (if c then a else b) : τ А {x:τ} e:σ (Abs) A λx.e: τ σ А f:σ τ; А x:σ (App) A (f x): τ А u:σ; А {x:σ} e:τ (Let) A (let x = u in e):τ А x:.τ (Spec) σ A x:[σ/ ].τ

20 ©2008 Сошников Д.В. 20 x: x: x: λx.x : (abs) x:,3:num λx.x : x:,3:num λx.x : int int (spec) x:,3:num (λx.x)3 : num (app) λx.x (λx.x)3

21 ©2008 Сошников Д.В. 21 (λf.f 3)(λx.x) : int {3:int} (λf.f 3) : (int σ) σ(λx.x) : {f:int σ,3:int} (f 3) : σ {f:int σ,3:int} f:int σ; {f:int σ,3:int} 3:int (app) (abs) (app) (abs) {x: } x: