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 -> t1
lub (t1 -> t2) -> (t1 -> t2)
gdzie t1
i t2
są zmiennymi typu.
Nie mogę wymyślić sposobu, w jaki można uzyskać coś takiego t1 -> t2
lub 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.)