Jakie są praktyczne problemy z typami skrzyżowań i złączy?

Projektuję prosty funkcjonalny język programowania o typie statycznym jako sposób uczenia się.

Wygląda na to, że system typów, który do tej pory wdrożyłem, może (przy odrobinie dodatkowej pracy) zawierać typy skrzyżowań i złączy, np. Możesz mieć:

• <Union String Integer>
• <Union Integer Foo>
• Przecięcie dwóch powyższych typów byłoby równiną Integer
• Połączenie tych dwóch typów byłoby <Union String Integer Foo>

Fakt, że jest to możliwe, oczywiście nie musi oznaczać, że jest to dobry pomysł na projekt. W szczególności jestem nieco zaniepokojony trudnościami implementacyjnymi związanymi z utrzymywaniem rozłączności typów i / lub obsługą nakładania się.

Jakie są zalety / wady stosowania takich funkcji w systemie typów?

Oto kilka rzeczy, o których należy pamiętać:

• Chociaż ogólnie uważamy, że wiemy, co rozumiemy przez teoretyczne zestawienie skrzyżowania i połączenia, istnieje kilka różnych podejść do tego, czym dokładnie są typy skrzyżowania i połączenia . Warto więc przypiąć to przed rozpoczęciem implementacji.
• Jednym z elementów, który moim zdaniem jest niezwykle ważny dla zrozumienia skrzyżowań i związków, jest koncepcja uszczegółowienia typu , zasadniczo idea, że ​​program ma pewien swoisty „archetyp” (np. „ Foo jest funkcją od liczb całkowitych do liczb całkowitych”), która może następnie dopracuj, aby wyrażać bardziej precyzyjne właściwości (np. „ foo przenosi liczby całkowite na parzyste liczby całkowite i nieparzyste liczby całkowite na nieparzyste liczby całkowite”). Przy koncepcji udoskonalenia kluczową właściwością, która odróżnia skrzyżowania i związki od produktów i sum, jest to, że skrzyżowanie / połączenie dwóch typów można utworzyć tylko wtedy, gdy udoskonalą ten sam archetyp. Innymi słowy, reguły formowania typu dla skrzyżowań i związków mogą być wyrażone w ten sposób (czytaj „$S \sqsubset A$„as” uściśla ”) podczas gdy zasady formowania zwykłych produktów i sum są następujące: $S$$A$ $$\frac{S\sqsubset A \quad T \sqsubset A}{S\cap T\sqsubset A}\qquad \frac{S\sqsubset A \quad T \sqsubset A}{S\cup T\sqsubset A}$$ $$\frac{S\sqsubset A \quad T \sqsubset B}{S* T\sqsubset A*B}\qquad \frac{S\sqsubset A \quad T \sqsubset B}{S+T\sqsubset A+B}$$
• Ponieważ skrzyżowań i związków można używać do dokładniejszych stwierdzeń na temat zachowania programu w czasie wykonywania, naturalne jest, że pisanie staje się wrażliwe na kolejność oceny. Na przykład w dokumentach (2) i (4) poniżej wyjaśniono, dlaczego „oczywiste” (i dość standardowe) zasady pisania i podtypów dla skrzyżowań i związków są w rzeczywistości niesłuszne dla języków podobnych do ML (ze względu na występowanie skutków ubocznych i nie zakończenie). Zostałeś ostrzeżony!
• Z podobnych powodów globalne wnioskowanie o typach na ogół staje się niepraktyczne lub nierozstrzygalne. Rzeczywiście, cała koncepcja „typu głównego” jest prawdopodobnie czerwonym śledziem, ponieważ funkcja może spełniać wiele różnych właściwości, które są nieistotne dla jej zamierzonego zastosowania (np. „ Foo przyjmuje liczby całkowite do liczb całkowitych większych niż 7”). Zamiast tego praktyczne podejście do skrzyżowań i związków (patrz (3) , (4) ) opiera się zasadniczo na połączeniu wnioskowania i sprawdzania.

Przypuszczam, że niektóre z powyższych punktów mogą brzmieć negatywnie, chociaż nie nazwałbym ich „minusami”, a jedynie „rzeczywistością” typów skrzyżowań i związków. Z drugiej strony, z punktu widzenia projektowania języka, jednym z powodów, dla których trzeba podejmować wysiłek wspierania skrzyżowań i związków (i ich poprawiania!) Jest to, że pozwalają one na bardziej precyzyjne wyrażanie właściwości programów w sposób przyrostowy, wymagając znacznie mniej drastyczna transformacja niż, powiedzmy, teoria typów zależnych.

Krótka lista lektur:

1. Projekt języka programowania Forsythe autorstwa Johna C. Reynoldsa
2. Rodzaje skrzyżowań i efekty obliczeniowe Rowan Davies i Frank Pfenning
3. Praktyczne sprawdzanie poprawności typu przez Rowan Davies (rozprawa doktorska)
4. Tridirectional Typechecking przez Joshua Dunfield i Frank Pfenning