Polimorfizm wyższego rzędu w porównaniu z typami nieopakowanymi

Mam język, w którym typy są domyślnie rozpakowane, a wnioskowanie typu oparte jest na Hindley-Milner. Chciałbym dodać polimorfizm wyższego rzędu, głównie do pracy z typami egzystencjalnymi.

Wydaje mi się, że rozumiem, jak sprawdzić te typy, ale nie jestem pewien, co robić podczas kompilacji. Obecnie kompiluję definicje polimorficzne, generując specjalizacje, podobnie jak szablony C ++, dzięki czemu mogą one pracować z wartościami rozpakowanymi. Na przykład, biorąc pod uwagę definicję f<T>, jeśli wywołuje tylko programowe f<Int32>i f<Char>, następnie pojawiają się tylko te specjalizacje w skompilowanym programie. (Na razie zakładam kompilację całego programu).

Ale przekazując funkcję polimorficzną jako argument, nie widzę, w jaki sposób mogę wygenerować odpowiednią specjalizację statycznie, ponieważ funkcję tę można wybrać w czasie wykonywania. Czy nie mam wyboru, jak użyć reprezentacji w ramkach? Czy istnieje sposób na rozwiązanie tego problemu?

Moją pierwszą myślą było zakodowanie polimorfizmu rang n jako ranga 1, ale nie sądzę, aby było to w ogóle możliwe, ponieważ formuła w logice konstruktywnej niekoniecznie musi mieć wcześniejszą normalną formę.

Myślałem o tym trochę. Głównym problemem jest to, że ogólnie nie wiemy, jak duża jest wartość typu polimorficznego. Jeśli nie masz tych informacji, musisz je jakoś zdobyć. Monomorfizacja otrzymuje te informacje, specjalizując się w polimorfizmie. Boks otrzymuje te informacje, umieszczając wszystko w reprezentacji o znanej wielkości.

Trzecią alternatywą jest śledzenie tego rodzaju informacji. Zasadniczo można wprowadzić inny rodzaj dla każdego rozmiaru danych, a następnie można zdefiniować funkcje polimorficzne dla wszystkich typów określonego rozmiaru. Naszkicuję taki system poniżej.

$$\newcommand{\bnfalt}{\;\;|\;\;} \newcommand{\rule}[2]{{\mathord{\array{#1}} \over {\mathord{#2}}}} \newcommand{\judge}[3]{{#1} \vdash {#2} : {#3}}$$ $$\begin{array}{llcl} \mbox{Kinds} & \kappa & ::= n \\ \mbox{Type constructors} & A & ::= & \forall a:\kappa.\; A \bnfalt \alpha \bnfalt A \times B \bnfalt A + B \bnfalt A \to B \\ & & | & \mathsf{ref}\;A \bnfalt \mathsf{Pad}(k) \bnfalt \mu \alpha:\kappa.\; A\\ \end{array}$$

Tutaj idea wysokiego poziomu polega na tym, że rodzaj tekstu mówi, ile słów potrzeba, aby ułożyć obiekt w pamięci. Dla każdego danego rozmiaru łatwo jest być polimorficznym we wszystkich typach tego konkretnego rozmiaru. Ponieważ każdy typ - nawet polimorficzny - nadal ma znany rozmiar, kompilacja nie jest trudniejsza niż w przypadku C.

$$\rule{ \alpha:n \in \Gamma} { \judge{\Gamma}{\alpha}{n} } \qquad \rule{ \judge{\Gamma, \alpha:n}{A}{m} } { \judge{\Gamma}{\forall \alpha:n.\; A}{m} }$$ $$\rule{ \judge{\Gamma}{A}{n} & \judge{\Gamma}{B}{m} } { \judge{\Gamma}{A \times B}{n + m} } \qquad \rule{ \judge{\Gamma}{A}{n} & \judge{\Gamma}{B}{n} } { \judge{\Gamma}{A + B}{n + 1} }$$ $$\rule{ \judge{\Gamma}{A}{m} & \judge{\Gamma}{B}{n} } { \judge{\Gamma}{A \to B}{1} } \qquad \rule{ \judge{\Gamma}{A}{n} } { \judge{\Gamma}{\mathsf{ref}\;A}{1} }$$ $$\rule{ } { \judge{\Gamma}{\mathsf{Pad}(k)}{k} } \qquad \rule{ \judge{\Gamma, \alpha:n}{A}{n} } { \judge{\Gamma}{\mu \alpha:n.\; A}{n} }$$

$A \times B$$A$$B$

Odnośniki są interesujące - wskaźniki są zawsze jednym słowem, ale mogą wskazywać na wartości dowolnej wielkości. Pozwala to programistom na implementację polimorfizmu do dowolnych obiektów przez boksowanie, ale nie wymaga od nich tego. Wreszcie, gdy w grę wchodzą wyraźne rozmiary, często przydatne jest wprowadzenie rodzaju wypełnienia, który wykorzystuje miejsce, ale nic nie robi. (Jeśli więc chcesz wziąć rozłączną sumę liczby całkowitej i pary liczb całkowitych, musisz dodać dopełnienie pierwszej liczby wewnętrznej, aby układ obiektu był jednolity.)

Typy rekurencyjne mają standardową regułę formowania, ale należy pamiętać, że wystąpienia rekurencyjne muszą być tego samego rozmiaru, co oznacza, że ​​zwykle trzeba je nakleić wskaźnikiem, aby można było wykonać sortowanie. Np. Typ danych listy można przedstawić jako

$$\mu \alpha:1.\; \mathsf{ref}\;(\mathsf{Pad}(2) + \mathsf{int} \times \alpha)$$

Oznacza to więc pustą wartość listy lub parę liczb całkowitych i wskaźnik do innej połączonej listy.

Sprawdzanie typu dla takich systemów również nie jest bardzo trudne; algorytm w mojej pracy ICFP z Joshua Dunfieldem, Pełne i łatwe dwukierunkowe sprawdzanie typów polimorfizmu wyższego stopnia dotyczy tego przypadku bez prawie żadnych zmian.

Wydaje się, że jest to bliższe problemowi kompilacji niż problemowi „teoretycznej informatyki”, więc prawdopodobnie lepiej jest zapytać gdzie indziej.

W ogólnym przypadku myślę, że nie ma innego rozwiązania niż użycie reprezentacji w ramkach. Ale spodziewam się również, że w praktyce istnieje wiele różnych alternatywnych opcji, w zależności od specyfiki twojej sytuacji.

Np. Niskopoziomową reprezentację nieopakowanych argumentów można zazwyczaj podzielić na kilka alternatyw, np. Liczby całkowite lub podobne, zmiennoprzecinkowe lub wskaźnik. Tak więc dla funkcji f<T>może naprawdę potrzebujesz wygenerować tylko 3 różne implementacje rozpakowane i możesz reprezentować polimorficzną jako krotkę tych 3 funkcji, więc utworzenie T do Int32 oznacza po prostu wybranie pierwszego elementu krotki, ...