Zdefiniuj listę, używając tylko systemu typów Hindley-Milner

Pracuję na małym kompilatorze rachunku lambda, który ma działający system wnioskowania typu Hindleya-Milnera, a teraz obsługuje także rekurencyjne let (nie w połączonym kodzie), co, jak rozumiem, powinno wystarczyć, aby Turing był kompletny .

Problem polega na tym, że nie mam pojęcia, jak to zrobić, aby obsługiwał listy lub czy już je obsługuje i po prostu muszę znaleźć sposób, aby je zakodować. Chciałbym móc je zdefiniować bez konieczności dodawania nowych reguł do systemu typów.

Najprostszym sposobem, w jaki mogę wymyślić listę, xjest coś, co jest albo null(albo pustą listą), albo parą zawierającą zarówno xlistę, jak i listę x. Ale aby to zrobić, muszę być w stanie zdefiniować pary i lub, które moim zdaniem są produktem i typami sum.

Wydaje się, że mogę zdefiniować pary w ten sposób:

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

Ponieważ pairmiałby typ a -> (b -> ((a -> (b -> x)) -> x)), po przejściu, powiedzmy, an inti a string, (int -> (string -> x)) -> xdałby coś z typem , co byłoby reprezentacją pary inti string. Niepokoi mnie to, że jeśli reprezentuje parę, to dlaczego nie jest to logicznie równoważne ani nie sugeruje zdania int and string? Jest to jednak równoważne (((int and string) -> x) -> x), jak gdybym mógł mieć tylko typy produktów jako parametry funkcji. Ta odpowiedźwydaje się, że rozwiązuje ten problem, ale nie mam pojęcia, co oznaczają symbole, których używa. Ponadto, jeśli tak naprawdę nie koduje typu produktu, czy jest coś, co mogę zrobić z typami produktów, których nie mogę zrobić z powyższą definicją par (biorąc pod uwagę, że mogę również zdefiniować n-krotki w ten sam sposób)? Jeśli nie, czy nie byłoby to sprzeczne z faktem, że nie można wyrazić koniunkcji (AFAIK) przy użyciu samej implikacji?

A może typ sumy? Czy mogę jakoś zakodować go przy użyciu tylko typu funkcji? Jeśli tak, czy wystarczyłoby to do zdefiniowania list? Albo czy jest jakiś inny sposób definiowania list bez konieczności rozszerzania mojego systemu typów? A jeśli nie, jakie zmiany musiałbym wprowadzić, jeśli chcę, aby było to tak proste, jak to możliwe?

Proszę pamiętać, że jestem programistą komputerowym, ale nie jestem informatykiem ani matematykiem i nieźle czytam notację matematyczną.

Edycja: Nie jestem pewien, jaka jest nazwa techniczna tego, co do tej pory zaimplementowałem, ale wszystko, co mam, to w zasadzie kod, który podłączyłem powyżej, który jest algorytmem generującym ograniczenia, który wykorzystuje reguły dla aplikacji, pobranych abstrakcji i zmiennych z algorytmu Hinleya-Milnera, a następnie algorytmu unifikacji, który otrzymuje typ główny. Na przykład wyrażenie \a.azwróci typ a -> a, a wyrażenie \a.(a a)wyrzuci błąd sprawdzania. Na dodatek nie istnieje dokładnie letreguła, ale funkcja, która wydaje się mieć ten sam efekt, który pozwala zdefiniować rekurencyjne funkcje globalne, takie jak ten pseudo-kod:

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.
}

Kod zasadniczo pobiera typ terminu, jak zwykle, ale przed ujednoliceniem dodaje do definicji zakresu nazwę funkcji zdefiniowanej za pomocą typu fikcyjnego, dzięki czemu można z niej korzystać rekurencyjnie.

Edycja 2: Właśnie zdałem sobie sprawę, że potrzebuję również typów rekurencyjnych, których nie mam, aby zdefiniować listę tak, jak chcę.

Pary

To kodowanie jest kościelnym kodowaniem par. Podobne techniki mogą kodować wartości logiczne, liczby całkowite, listy i inne struktury danych.

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

pairjest konstruktorem typu pary firsti secondjest destruktorami. (Są to te same słowa, których używa się w programowaniu obiektowym; tutaj słowa mają znaczenie związane z logiczną interpretacją typów i terminów, których nie będę tutaj omawiać.) Intuicyjnie, destruktory pozwalają ci uzyskać dostęp do tego, co jest w obiekcie, a konstruktory torują drogę niszczycielowi, przyjmując jako argument funkcję, którą stosują do części obiektu. Zasadę tę można zastosować do innych typów.

Sumy

Kodowanie dyskryminowanego związku przez Kościół jest zasadniczo podwójne w stosunku do kodowania pary przez Kościół. Jeśli para składa się z dwóch części, które należy połączyć, i możesz wybrać wyodrębnienie jednej lub drugiej, możesz zbudować związek na jeden z dwóch sposobów, a kiedy go użyjesz, musisz zezwolić na oba sposoby. Istnieją więc dwa konstruktory i jeden destruktor, który przyjmuje dwa argumenty.

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)

Pozwól mi skrócić ten typ (a->t) -> (b->t) -> tjako SUM(a,b)(t). Następnie typy niszczycieli i konstruktorów to:

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

A zatem

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

Listy

W przypadku listy zastosuj ponownie tę samą zasadę. Listę, której elementy mają typ, amożna zbudować na dwa sposoby: może to być pusta lista lub element (głowa) plus lista (ogon). W porównaniu z parami, jest trochę skręcają gdy chodzi o destruktorów: nie można mieć dwa oddzielne destruktorów headi taildlatego będą pracować tylko na niepustych list. Potrzebujesz pojedynczego destruktora z dwoma argumentami, z których jeden jest funkcją 0-argumentową (tj. Wartością) dla przypadku zerowego, a drugi funkcją 2-argumentową dla przypadku przeciwnego. Funkcje podoba is_empty, headi tailmogą pochodzić z tego. Podobnie jak w przypadku sum, lista jest bezpośrednio własną funkcją destruktora.

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)

consconscons$T$$T_1,\ldots,T_n$

Jak przypuszczasz, jeśli chcesz zdefiniować typ, który zawiera tylko jednorodne listy, potrzebujesz typów rekurencyjnych. Dlaczego? Spójrzmy na typ listy. Lista jest kodowana jako funkcja, która przyjmuje dwa argumenty: wartość zwracaną na pustych listach oraz funkcję obliczającą wartość zwracaną w komórce przeciwnej. Niech abędzie typem elementu, btypem listy i ctypem zwracanym przez destruktor. Typ listy to

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

Ujednolicenie listy oznacza, że ​​jeśli jest to wada, ogon musi mieć ten sam typ co całość, tzn. Dodaje ograniczenie

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

System typów Hindley-Milner można rozszerzyć o takie typy rekurencyjne, a faktycznie robią to praktyczne języki programowania. Praktyczne języki programowania nie pozwalają na takie „nagie” równania i wymagają konstruktora danych, ale nie jest to nieodłączny wymóg leżący u podstaw teorii. Wymaganie konstruktora danych upraszcza wnioskowanie o typach, aw praktyce unika się akceptowania funkcji, które faktycznie są błędne, ale zdarza się, że można je wpisać z pewnym niezamierzonym ograniczeniem, które powoduje trudny do zrozumienia błąd typu, gdy funkcja jest używana. Dlatego na przykład OCaml akceptuje niestrzeżone typy rekurencyjne tylko z domyślną -rectypesopcją kompilatora. Oto powyższe definicje w składni OCaml, wraz z definicją typu dla list jednorodnych przy użyciu notacji dlaaliasowane typy rekurencyjne : type_expression as 'aoznacza, że ​​typ type_expressionjest zunifikowany ze zmienną '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

Marszczenie

Patrząc na to nieco bardziej ogólnie, jaka jest funkcja reprezentująca strukturę danych?

• $n$$n$
• $(x,y)$$x$$y$
• $\mathrm{in}_i(x)$$i$$x$
• $[x_1,\ldots,x_n]$

Ogólnie rzecz biorąc, struktura danych jest reprezentowana jako funkcja składania . Jest to ogólna koncepcja dla struktur danych: funkcja składania jest funkcją wyższego rzędu, która przenika strukturę danych. Z technicznego punktu widzenia fold jest uniwersalny : wszystkie „ogólne” przejścia w strukturze danych można wyrazić jako fold. Struktura danych może być reprezentowana, gdy pokazuje to funkcja składania: wszystko, co musisz wiedzieć o strukturze danych, to jak ją przechodzić, reszta to szczegół implementacji.

Możesz reprezentować typy sum jako typy produktów z tagami i wartościami. W tym przypadku możemy trochę oszukać i użyć jednego znacznika do przedstawienia wartości zerowej lub nie, mając drugi znacznik reprezentujący parę głowa / ogon.

Logiczne definiujemy w zwykły sposób:

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

Lista jest wtedy parą z pierwszym elementem jako wartość logiczną, a drugim elementem jako para głowa / ogon. Niektóre podstawowe funkcje listy:

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) ) )