Haskell, 04 лекция (от 19 октября)

Материал из eSyr's wiki.

Каррирование: если есть функция, принимающая два параметра, то каррированием мы будем называть подстановку только одного параметра: f(i, j), f(3) → f(j)

например, можно взять один из комбинаторов, который рассм. в прошлый раз: Sxyz = xz(yz), он будет иметь следующий тип: (a → b → c) → (b → b) → a → c. Как это получается: ... .

Таким образом, тип функции опр. на языках, которые след.данной модели типизации, напр., язык haskell. Если в нём сказать :t s, то он выдал примерно то же самое.

Какие возн. с этим проблемы? Пусть у нас есть комбинатор тождества I=λx.x. Согласно нашему пред. опр., мы должны приписать к нему тип. Он будет иметь тип α → xα. Но какой тип имеет x? Ведь ему всё равно, какой арг. ему передали, он его возвр. Есть неск. подходов решения этой рпоблемы, мы рассм. подход Карри. То есть, он имеет тип, но в некотором контексте. например, контексте IF ((λx.x) TrUE) ((λx.x)3) ((λxx) 4), то в первом контексте будет boolean, во втором - 3б в третьем - 4. Конеткст — множество правил, которые мы знаем, мн-во имеющихся типов для функции. Это множество вида: Γ = {x:τ, ...}. Тогда запишем правило вывода типов в след. виде:

1. x:α ∈ Γ ⇒ Γ |- x:α
2. c: σ
3. Если в контексте имеется правило выид Γ |- s:&sigma → τ, Γ |- t:σ ⇒ &Gamm; |- st:τ
4. Правило для абстракции: Γ ∪ {x:α} |- t:τ ⇒ Γ |- λxt:α→ t

Это практичски то же самое, но ...

На втором курсе в курсе ООП разбирались шаблоны в С++б они очень схожи с данным определением.

Мощь такой констр. настоько велика, что сам по себе вывод типов явл. Тьюринг-полным, примером явл. метапрогр. на шаблонах C++, C++TMP.

Какие в св. с типизацией могут возн. проблемы: нек-рые выр. типа иметь не будут. Доказывается, что если у нас есть нек-рый тип σ, нек-рый τ, и тип σ → τ, тог Γ |- t:σ ⇒ Γ |/- t:σ→τ

При этом вывести тип у Y-комбинатора не очень получится.

С целью инт. в язык стат. типизацию, интерпретатор вводятся другие понятия, напр., мы можем расш. этот список правил одни или неск. правилами, позв. описывать стр. данных, напр., написать доп. правило для дек. произв.

Так или иначе, это модель, исп. в стат. типизир. языках, напр., haskell

Настало время разобрать, как запис. ф-ции в haskell.

Давным-давно мы разб. оператор if:

if True x y = x
if False x y = y

К нему была приписана такая штука:

if: Bool → a → a → a

Что такое a? Параметризованный тип. Какой именно — будет зависеть от контекста. Если запишем (if True 3 4), то a будет Int, и всё выражение будет иметь тип Int.

Какого ещё понятия не хв. для перехода к языку? Что такое ф. программа? Это сущность, которая даные переводит в другие данные. Проблема такого подхода в том, что в совр. арх. есть такая сущность как файл. Для представления файлов и др. понадобится такая штука, как монады. Это понятие, позаимст. из теории категорий. В теор. категорий категория это некий абстр. набор объектов, в котором мы опр. абстр. операцию. То что мы наз. операцией, в т. к. наз. морфизм. Что такое морфизм: пусть есть два объекта, и морфизм это некая стрелка, которую мы записываем между ними: a, b: a → b.

Что ещё мы опр. Пусть есть два морфизма: f: a → b, g: b → c, тогда композиция морфизмов — стрелка из a в c: h = g · f: h=a→ c.

id: a → a, id · f = f, g · id = g.

Как правило мы говорим об объектах, которые принадл. множеству, и ...

Пример категории: множество всех множеств с операциями над ними.

Менее абстр. примером явл. мн.-во чисел [0..1], морфизмом может явл. операция меньше.

В такой системе можно ввести понятие изоморфизма: такой морфизм: f: a→b, g: b→a, то если f·g=id, g·f=id, то f, g - изоморфизм.

Теориякат. абстр. до такой степени, что можно предст. категорию категории, вопрос в том, что будет явл. морфизмом. Для этого введём понятие функтора. Пусть есть две категории, X, Y. И есть нек-рый морфизм F: X→Y. Что значит эта запись? Это означает, что для каждого объекта из X существует объект из Y, который сопоставлен объекту из X, и для каждого морфизма из первой кат. сущ. сопост. ему морфизм из второй категории:

∀ a∈ X &exists; F(a)∈Y
∀ f ∈ X &exists;F(f)∈Y

1. X: f a→ b⇒Y:F(f): F(a) →F(b)
2. X id_X → Y id_Y = Fid_Y)
3. X: f: a→b, g:b→c ⇒ Y: F(g·f)=F(g)·F(f)
4. X: f

Пусть есть три категории и два функтора:

X, Y, Z
F: X → Y
G: Y → Z
(G·F) X→ Z

id: R→R
x∈Z: R → (x,R)

Натуральное преобразование: пусть есть F: X→Y, G:X→Y. тогда

φ: F→G
∀x∈X &exists; φ(x) F(x)→G(x) ∈ Y

a,b∈X ∀f: a→b φ(a): G(F)=F(f)·φ(b)

Графич. это можно предст. так:

F(a) →^F(f) F(b) →^φ(b) G(b)
F(a) →^φ(a) G(a) →^G(f) G(b)

Что такое монады? Монада — функтор F с двумя естественными трансформациями:

X F X→X

Рассмотрим категорию компл. чисел, категорию пар чисел. Если в C опр. морфизм из a в b, то получим ест. транс. из точки a в точку b:

C: f: a→ b
   Point_a → Point;_b

что такое монады? Монада в категории C это функтор из C в C с двумя ест. трансформациями:

F: C→C
     u: 1→F
     m: F·F→F

Назовём F(u) транформацию следующего вида:

F(u): F → F·F
F(m): (f·F) F → F·F

В таком случае можно сказать, что:

1. Всегда выполняется

F(x) →^F(u_x) F(F(X))
     ?кфккж:ь_А(ч) F(X)
F(u)m = id

1. F(m)·m = n·m

F(F(F(x))) ...

Возьмём множество A и опр. функтор вида:

A X→(X×A)

Что это такое? Можно рассм. это как некоторый набор сост. выч. машины., то есть, (X×A) — все выч. магины раб. на X, выд. результат из X. То есть, все функции вида A→(A×X)

Мы получим, что такой набор машинных состояний это монада.

Как это доказать? Нужно опр. u, m:

u_x: X→(A×X)
m_x: (A×(A×X)) → (A×X)

Перыое преобр. переводит из X в множество .., что же до m, то здесь у нас имеется другой набор маш. сост., где A — набор сост., который имеет выводом другой набор маш. состояний.

Что мы получили? Что если мы рассм. прогр. как функцию, а если ещё доб. понятие сост., то в него мы можем положить неск. большее, чем просто неизм. объект, напр., моэжно сказать, что в сост. вх. нек-рый объект ... . Например, можно ассоц. с моадой файл и работать с ним, не теряя мат. описания того, что происходит.

Другим примером исп. монад в ЯП явл. иск. Обычно, в семантике λ-исчисл. нам трудно опр. искл. ситуации. Одно из решений — опр. нулевого объекта, и если наша функция не детерм. для всего входа, мы записали её таким обр., что не можем сказать, что она имеет рез-т для всякого ввода. Например, выч. полож. чисел. Тогда обл. значений будет мн-во оплож. зн. и нулевое значение, и его мы завернём в монаду.

В след раз уже Артём не будет, в след. раз будет уже введение в Haskell, введение в синтаксис.