Определить список, используя только систему типов Хиндли-Милнера

Я работаю над небольшим компилятором лямбда-исчисления, который имеет работающую систему логического вывода типа Хиндли-Милнера, а теперь также поддерживает рекурсивный метод давайте (не в связанном коде), который, как я понимаю, должно быть достаточно для завершения Тьюринга .

Проблема сейчас в том, что я понятия не имею, как создать списки поддержки или уже поддерживает их, и мне просто нужно найти способ их кодирования. Я хотел бы иметь возможность определять их без добавления новых правил в систему типов.

Самый простой способ, которым я могу представить список, x- это что-то, что есть null(или пустой список), или пара, которая содержит как xи, так и список x. Но для этого мне нужно уметь определять пары и или, которые, как я считаю, являются продуктом и типом суммы.

Кажется, я могу определить пары таким образом:

pair = λabf.fab
first = λp.p(λab.a)
second = λp.p(λab.b)

Так как pairбудет иметь тип a -> (b -> ((a -> (b -> x)) -> x)), после передачи, скажем, a intи a string, он даст что-то с типом (int -> (string -> x)) -> x, который будет представлением пары intи string. Что меня здесь беспокоит, так это то, что если это представляет пару, то почему это логически не эквивалентно и не подразумевает предложение int and string? Тем не менее, это эквивалентно (((int and string) -> x) -> x), как если бы я мог иметь только типы продуктов в качестве параметров для функций. Этот ответпохоже, решают эту проблему, но я понятия не имею, что означают символы, которые он использует. Кроме того, если это на самом деле не кодирует тип продукта, могу ли я что-то сделать с типами продуктов, которые я не смог бы сделать с моим определением пар выше (учитывая, что я также могу определять n-кортежи таким же образом)? Если нет, не будет ли это противоречить тому факту, что вы не можете выразить (AFAIK) соединение, используя только подтекст?

Кроме того, как насчет типа суммы? Можно ли как-то кодировать его, используя только тип функции? Если так, будет ли этого достаточно для определения списков? Или еще, есть ли другой способ определения списков без необходимости расширять мою систему типов? И если нет, то какие изменения мне нужно было бы сделать, если я хочу сделать это как можно более простым?

Пожалуйста, имейте в виду, что я программист, но не ученый и не математик, и довольно плохо читаю математические записи.

Изменить: я не уверен, что техническое название того, что я реализовал до сих пор, но все, что у меня есть, это в основном код, который я связал выше, это алгоритм генерации ограничений, который использует правила для приложений, абстракций и взятых переменных из алгоритма Хинли-Милнера, а затем алгоритм объединения, который получает основной тип. Например, выражение \a.aвыдаст тип a -> a, а выражение \a.(a a)сгенерирует ошибку проверки возникновения. Помимо этого, существует не совсем letправило, а функция, которая, по-видимому, имеет тот же эффект, который позволяет вам определять рекурсивные глобальные функции, такие как этот псевдокод:

GetTypeOfGlobalFunction(term, globalScope, nameOfFunction)
{
    // Here 'globalScope' contains a list of name-value pair where every value is of class 'ClosedType', 
    // meaning their type will be cloned before unified in the unification algorithm so that they can be used polymorphically 
    tempType = new TypeVariable() // Assign a dummy type to `tempType`, say, type 'x'.
    // The next line creates an scope with everything in 'globalScope' plus the 'nameOfFunction = tempType' name-value pair
    tempScope = new Scope(globalScope, nameOfFunction, tempType) 
    type = TypeOfTerm(term, tempScope) // Calculate the type of the term 
    Unify(tempType, type)
    return type
    // After returning, the code outside will create a 'ClosedType' using the returned type and add it to the global scope.
}

Код в основном получает тип термина как обычно, но перед объединением он добавляет имя функции, определяемой с помощью фиктивного типа, в область действия типа, чтобы его можно было использовать изнутри самого себя рекурсивно.

Редактировать 2: Я только что понял, что мне также понадобятся рекурсивные типы, которых у меня нет, чтобы определить список так, как я хочу.

Пары

Эта кодировка является церковной кодировкой пар. Подобные методы могут кодировать логические значения, целые числа, списки и другие структуры данных.

x:a; y:bpair x y(a -> b -> t) -> t$\to$$\vee$$\wedge$$\neg$$\iff$

pairявляется конструктором для парного типа и firstи secondявляются деструкторами. (Это те же слова, которые используются в объектно-ориентированном программировании; здесь слова имеют значение, связанное с логической интерпретацией типов и терминов, которые я не буду здесь описывать.) Интуитивно, деструкторы позволяют вам получить доступ к тому, что в объекте и конструкторы прокладывают путь деструктору, принимая в качестве аргумента функцию, которую они применяют к частям объекта. Этот принцип может быть применен к другим типам.

Суммы

Церковная кодировка дискриминируемого союза по сути двойственна церковной кодировке пары. Если пара состоит из двух частей, которые необходимо соединить, и вы можете выбрать извлечение одной или другой, вы можете создать объединение одним из двух способов, и при его использовании необходимо предусмотреть оба пути. Таким образом, есть два конструктора, и есть один деструктор, который принимает два аргумента.

let case w = λf. λg. w f g           case : ((a->t) -> (b->t) -> t) -> (a->t) -> (b->t) -> t
  (* or simply let case w = w *)
let left x = λf. λg. f x             left : a -> ((a->t) -> (b->t) -> t)
let right y = λf. λg. g x            right : b -> ((a->t) -> (b->t) -> t)

Позвольте мне сократить тип (a->t) -> (b->t) -> tкак SUM(a,b)(t). Тогда типы деструкторов и конструкторов:

case : SUM(a,b)(t) -> (a->t) -> (b->t) -> t
left : a -> SUM(a,b)(t)
right : b -> SUM(a,b)(t)

таким образом

case (left x) f g → f x
case (rightt y) f g → g y

Списки

Для списка примените снова тот же принцип. Список, элементы которого имеют тип, aможет быть построен двумя способами: это может быть пустой список, или это может быть элемент (голова) плюс список (хвост). По сравнению с парами, есть немного поворот , когда дело доходит до деструкторов , вы не можете иметь два отдельных деструкторов headи tailпотому , что они будут работать только на непустых списках. Вам нужен один деструктор с двумя аргументами, один из которых является функцией с 0 аргументами (то есть значением) для случая nil, а другой - с 2 аргументами для случая cons. Функции, как is_empty, headи tailмогут быть получены из этого. Как и в случае сумм, список является непосредственно его собственной функцией-деструктором.

let nil = λn. λc. n
let cons h t = λn. λc. c h t
let is_empty l = l true (λh. λt. false) 
let head l default = l default (λh. λt. h)
let tail l default = l default (λh. λt. t)

Каждая из этих функций является полиморфной. Если вы работаете с типами этих функций, вы заметите, что это не consявляется одинаковым: тип результата не совпадает с типом аргумента. Тип результата - переменная - она ​​более общая, чем аргумент. Если вы объединяете consвызовы, последовательные вызовы для создания списка создаются consв разных типах. Это важно, чтобы списки работали в отсутствие рекурсивных типов. Таким способом вы можете создавать гетерогенные списки. На самом деле типы, которые вы можете выразить, не являются «списком$T$$T_1,\ldots,T_n$

Как вы предполагаете, если вы хотите определить тип, который содержит только однородные списки, вам нужны рекурсивные типы. Почему? Давайте посмотрим на тип списка. Список кодируется как функция, которая принимает два аргумента: значение, возвращаемое в пустых списках, и функция, которая вычисляет значение, возвращаемое в ячейке cons. Позвольте aбыть типом элемента, bтипом списка и cтипом, возвращаемым деструктором. Тип списка

a -> (a -> b -> c) -> c

Создание списка однородным означает, что если это cons-ячейка, то хвост должен иметь тот же тип, что и целое, т. Е. Добавляет ограничение

a -> (a -> b -> c) -> c = b

Система типов Хиндли-Милнера может быть расширена такими рекурсивными типами, и на самом деле практические языки программирования делают это. Практические языки программирования, как правило, запрещают такие «голые» уравнения и требуют конструктора данных, но это не является внутренним требованием лежащей в основе теории. Требование конструктора данных упрощает вывод типов и на практике стремится избежать принятия функций, которые на самом деле содержат ошибки, но могут быть типизированными с некоторым непреднамеренным ограничением, которое вызывает трудную для понимания ошибку типа при использовании функции. Вот почему, например, OCaml принимает неохраняемые рекурсивные типы только с -rectypesопцией компилятора не по умолчанию . Вот определения выше в синтаксисе OCaml, вместе с определением типа для однородных списков с использованием нотации дляпсевдонимы рекурсивных типов : type_expression as 'aозначает, что тип type_expressionобъединен с переменной 'a.

# let nil = fun n c -> n;;
val nil : 'a -> 'b -> 'a = <fun>
# let cons h t = fun n c -> c h t;;
val cons : 'a -> 'b -> 'c -> ('a -> 'b -> 'd) -> 'd = <fun>
# let is_empty l = l true (fun h t -> false);;
val is_empty : (bool -> ('a -> 'b -> bool) -> 'c) -> 'c = <fun>
# let head l default = l default (fun h t -> h);;
val head : ('a -> ('b -> 'c -> 'b) -> 'd) -> 'a -> 'd = <fun>
# let tail l default = l default (fun h t -> t);;
val tail : ('a -> ('b -> 'c -> 'c) -> 'd) -> 'a -> 'd = <fun>
# type ('a, 'b, 'c) ulist = 'c -> ('a -> 'b -> 'c) -> 'c;;
type ('a, 'b, 'c) ulist = 'c -> ('a -> 'b -> 'c) -> 'c
# is_empty (cons 1 nil);;
- : bool = false
# head (cons 1 nil) 0;;
- : int = 1
# head (tail (cons 1 (cons 2.0 nil)) nil) 0.;;
- : float = 2.

(* -rectypes is required for what follows *)
# type ('a, 'b, 'c) rlist = 'c -> ('a -> 'b -> 'c) -> 'c as 'b;;
type ('a, 'b, 'c) rlist = 'b constraint 'b = 'c -> ('a -> 'b -> 'c) -> 'c
# let rcons = (cons : 'a -> ('a, 'b, 'c) rlist -> ('a, 'b, 'c) rlist);;
val rcons :
  'a ->
  ('a, 'c -> ('a -> 'b -> 'c) -> 'c as 'b, 'c) rlist -> ('a, 'b, 'c) rlist =
  <fun>
# head (rcons 1 (rcons 2 nil)) 0;;
- : int = 1
# tail (rcons 1 (rcons 2 nil)) nil;;
- : 'a -> (int -> 'a -> 'a) -> 'a as 'a = <fun>
# rcons 1 (rcons 2.0 nil);;
Error: This expression has type
         (float, 'b -> (float -> 'a -> 'b) -> 'b as 'a, 'b) rlist = 'a
       but an expression was expected of type
         (int, 'b -> (int -> 'c -> 'b) -> 'b as 'c, 'b) rlist = 'c

Складки

Если взглянуть на это более широко, какова функция, которая представляет структуру данных?

• Для натурального числа: $n$$n$
• $(x,y)$$x$$y$
• $\mathrm{in}_i(x)$$i$$x$
• $[x_1,\ldots,x_n]$

В общих чертах, структура данных представлена ​​как ее функция сгиба . Это общая концепция для структур данных: функция сгиба - это функция высшего порядка, которая пересекает структуру данных. Существует технический смысл, в котором сгиб универсален : все «общие» обходы структуры данных могут быть выражены через сгиб. То, что структура данных может быть представлена ​​в виде ее функции сгиба, показывает это: все, что вам нужно знать о структуре данных, это как ее обойти, остальное - деталь реализации.

Вы можете представлять типы сумм в виде типов продуктов с тегами и значениями. В этом случае мы можем немного обмануть и использовать один тег для представления нуля или нет, имея второй тег, представляющий пару голова / хвост.

Мы определяем логические значения обычным способом:

true = λi.λe.i
false = λi.λe.e
if = λcond.λthen.λelse.(cond then else)

Затем список представляет собой пару с первым элементом в качестве логического значения, а второй элемент в виде пары голова / хвост. Некоторые основные функции списка:

isNull = λl.(first l)
null = pair false false     --The second element doesn't matter in this case
cons = λh.λt.(pair true (pair h t ))
head = λl.(fst (snd l))   --This is a partial function
tail = λl.(snd (snd l))   --This is a partial function  

map = λf.λl.(if (isNull l)
                 null 
                 (cons (f (head l)) (map f (tail l) ) )