Dlaczego algorytm Hindleya-Milnera nigdy nie daje typu takiego jak t1 -> t2?

Czytam o algorytmie pisania Hindleya-Milnera podczas pisania implementacji i widzę, że tak długo, jak każda zmienna jest związana, zawsze otrzymasz albo typy atomowe, albo typy, w których argumenty określą typ końcowy, taki jak t1 -> t1lub (t1 -> t2) -> (t1 -> t2)gdzie t1i t2są zmiennymi typu.

Nie mogę wymyślić sposobu, w jaki można uzyskać coś takiego t1 -> t2lub po prostu t1, co rozumiem, że oznaczałoby to uszkodzenie algorytmu, ponieważ nie byłoby sposobu na określenie rzeczywistego rodzaju wyrażenia. Skąd wiesz, że nigdy nie dostaniesz takiego typu, jak te „zepsute”, o ile każda zmienna jest związana?

Wiem, że algorytm zwraca typy ze zmiennymi, ale zawsze są one rozwiązywane po przekazaniu argumentów do funkcji, czego nie byłoby w przypadku funkcji z typem t1 -> t2. Dlatego chcę wiedzieć, skąd wiemy, że algorytm nigdy nie da takich typów.

(Wygląda na to, że można uzyskać te „zepsute” typy w ML , ale pytam o rachunek lambda.)

$\forall \alpha,\beta.\; \alpha\mathbin\rightarrow\beta$$\forall \alpha.\; \alpha\mathbin\rightarrow\alpha$$\lambda x.x$

$\forall \alpha,\beta.\; \alpha\mathbin\rightarrow\beta$$\beta$$\beta$$\beta$$\beta$$\beta$

$\Delta = \lambda x. x \, x$$(\forall \alpha. \alpha) \rightarrow (\forall \alpha. \alpha)$$\Delta\,\Delta$

$\forall A, \forall B, A \Rightarrow B$$\forall \alpha,\beta.\; \alpha\mathbin\rightarrow\beta$

$Y$$Y (\lambda x.x)$$\forall \alpha. \alpha$$\forall A, \forall B, A \Rightarrow B$

Znalezienie cienkiej linii między systemami typów zapewniającymi silną normalizację a systemami typów, które nie są trudnym i interesującym problemem. Jest to ważny problem, ponieważ określa, która logika jest poprawna, innymi słowy, które programy zawierają dowody twierdzeń. Możesz pójść znacznie dalej niż System F, ale zasady stają się bardziej złożone. Na przykład rachunek konstrukcji indukcyjnych, który jest podstawą asystenta dowód Coq , silnie normalizuje się, ale jest w stanie opisać wspólne struktury danych indukcyjnych i algorytmy nad nimi, i więcej.

Gdy tylko dojdziesz do prawdziwych języków programowania, korespondencja się psuje. Prawdziwe języki programowania mają takie funkcje, jak ogólne funkcje rekurencyjne (które mogą się nie kończyć), wyjątki (wyrażenie, które zawsze wywołuje wyjątek, nigdy nie zwraca wartości, a zatem może mieć dowolny typ w większości systemów typów), typy rekurencyjne (które pozwalają na nieterminację zakraść się) itp.