- PVSM.RU - https://www.pvsm.ru -
В части 1 [1] мы говорили о том, какие строительные блоки нужны для формализации Хиндли-Милнера, а в этом посте мы конкретизируем их определения и сформулируем формализацию в целом:
Мы дадим рекурсивное определение [2] того, что такое выражение; другими словами, мы определим большую часть типов выражений, расскажем, как создавать новые, более сложные выражения, исходя из существующих, и покажем, что создавать таким способом можно только допустимые выражения.
e
— произвольное выражение, а x
— произвольная переменная, то λx.e
является выражением. Здесь поможет думать о e
, как об обычном (но не обязательно) сложном выражении, включающем в себя x
, т.е. x
²+2
, а затем о λx.e
как об анонимной функции, которая принимает на вход x
и возвращает результат вычисления выражения e
для заданного значения x
. Проще говоря, думайте об этом как о
function(x) { return x^2 + 2; }
f
и e
— допустимые выражения, то f(e)
также является допустимым. Оно называется «наложением» (Application) по очевидным причинам.x
— переменная, а e
1 и e
0 — допустимые выражения, то замена каждого вхождения x
в e
0 на e
1 также даст допустимое выражение. Т.е., если, например, e
1 = x
²+2
и e
0 = y/3
, то полагая x
= e
0 в e
1, мы получим выражение (y/3)
²+2
.e
0 в качестве x
в e
1 эквивалентна применению абстракции λx.
e
1 к e
0. Он добавлен только для поддержки так называемого let-полиморфизма [3].] Ничто более допустимым выражением не является.
В сторону: любой, кто уделит достаточно внимания этому вопросу, будет удивлён: «Минуточку, как мне сделать из этого какое-либо полезное выражение? Как мне получить x
2+2
(или хотя бы просто 2), исходя только из изложенного? Чёрт, а что на счёт нуля? В этих правилах нет ни строчки, очевидно приводящей к выражению 0». Решением в данном случае является создание выражения в лямбда-исчислении, которое ведёт себя как 0,1,…,+,×,−,/ при корректной интерпретации. Другими словами, нам следует закодировать числа, арифметические операции, строки и т.п. в шаблоны, которые мы можем создать с помощью лямбда-синтаксиса. В этом посте [4] есть маленький, но очень хороший раздел, посвящённый числам и арифметическим операциям. Это интереснейшая особенность лямбда-исчисления: у нас есть элементарный синтаксис, который мы можем рекурсивно определить четырьмя простыми пунктами, но он позволяет нам индуктивно доказать множество вещей в четыре основных шага, поскольку язык сам по себе обладает выразительной силой записывать числа, строки и все типы операций, которые только могут нам понадобиться.
Пусть e
— любое выражение, такое что "e
" — переменная в нашем мета-языка, обозначающая любое выражение из нашего базового языка. Например, такое, как любое из нижеследующих:
x
Math.pow(x,2)
[1,2].forEach ( function(x) { print(x); } )
Тогда, если t
— это произвольный тип, то мы можем выразить "e
имеет тип t
" через
e:t
Как и e
, t
— это переменная в нашем мета-языке, которая может соответствовать любому типу в базовом языке (Int, String и т.д.). И так же, как для e
, для t
соответствие какому-либо конкретному типу не является обязательным.
Можно дать и формальное определение того, что считать типом, как мы сделали выше для выражений. Однако, абстракция в этом случае получается довольно замысловатая, так что мы этот момент опустим. Я просто обращаю ваше внимание на два ключевых положения, которые следует держать в уме:
s
и t
— типы, то t
→s;
— это тип функции с t
на входе и s
на выходе r
— тип, возможно составленный из других типов (подобно тому, как t
→s
составляется из t
и s,
каждый из которых, в свою очередь, потенциально можно представить композицией ещё каких-то типов), а α
— переменная этого типа, то ∀α.r
является типом. function (x) { return x; }
Эта функция имеет тип String
→String
. Или Int
→Int
. Фактически, для любого типа t
её тип t
→t
. Мы будем говорить, что она имеет тип ∀t.t
→t
. Каждый из типов String
→String
или t
→t
является «монотипом». ∀t.t
→t
— это «политип». Функция, тождественная написанной выше, имеет абстрактный политип ∀t.t
→t
, который на практике означает, что для любого реального типа t
она имеет тип t
→t
. Собирая всё вышесказанное воедино, получим вот такую компактную резюмирующую запись:
λx.x:
∀α.α
→α
Сейчас мы хотим формализовать ветку правил о том, как от знания некоторых выражений и их типов нам перейти к выводу типов большего числа выражений. Помните, как исчисление высказываний формулирует Modus Ponens? Мы собираемся сделать нечто подобное. Например, допустим, что мы хотим формализовать следующую часть рассуждений:
Предположим, что я уже в состоянии вывести, что переменная
duck
имеет типAnimal
.
Более того, предположим, что я вывел, чтоspeak
— метод, имеющий типAnimal
->String
.
Тогда я могу вывести, чтоspeak(duck)
имеет типString
.И любые рассуждения, укладывающиеся в такую форму, — допустимый вывод типа.
Мы формализуем это следующим образом:
Это правило называется [App] (для наложений), и оно — одно из тех, что присутствуют в этом вопросе на StackOverflow [5]. О нём и оставшихся правилах мы поговорим в следующем посте. А пока давайте разберёмся со всеми символами, которые нам встретились выше:
x:t
означает, что если мы возьмём утверждение из Γ в качестве предположения/аксиомы/существующего знания, то мы можем вывести, что x
имеет тип t
. x:t
∈ Γ говорит о том, что высказывание x:t
принадлежит Γ. y
имеет тип σ из Γ, то мы можем вывести и то, что x
имеет тип τ из Γ. Следующий шаг:
Примечание переводчика: я буду очень признательна за любые замечания в личку по поводу перевода.
Автор: AveNat
Источник [7]
Сайт-источник PVSM.RU: https://www.pvsm.ru
Путь до страницы источника: https://www.pvsm.ru/programmirovanie/40981
Ссылки в тексте:
[1] части 1: http://habrahabr.ru/post/185362/
[2] рекурсивное определение: https://www.google.ru/url?sa=t&rct=j&q=&esrc=s&source=web&cd=2&cad=rja&ved=0CDAQFjAB&url=http%3A%2F%2Fru.wikipedia.org%2Fwiki%2F%25D0%25A0%25D0%25B5%25D0%25BA%25D1%2583%25D1%2580%25D1%2581%25D0%25B8%25D0%25B2%25D0%25BD%25D0%25BE%25D0%25B5_%25D0%25BE%25D0%25BF%25D1%2580%25D0%25B5%25D0%25B4%25D0%25B5%25D0%25BB%25D0%25B5%25D0%25BD%25D0%25B8%25D0%25B5&ei=hOHnUd3VHIXP4QSh24CIDQ&usg=AFQjCNHtw-THbq5A9M5Bg_exQgnY2jX29Q&sig2=YDaHgBdy6yVVB7gXnc9peA&bvm=bv.49478099,d.bGE
[3] let-полиморфизма: https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner#Let-polymorphism
[4] этом посте: http://palmstroem.blogspot.com/2012/05/lambda-calculus-for-absolute-dummies.html
[5] вопросе на StackOverflow: http://stackoverflow.com/questions/12532552/what-part-of-milner-hindley-do-you-not-understand
[6] Часть 3: http://habrahabr.ru/post/189446/
[7] Источник: http://habrahabr.ru/post/185686/
Нажмите здесь для печати.