W jaki sposób GHCi wybiera nazwy zmiennych typu?

Question

Podczas korzystania z interaktywnego GHC tłumacza, to jest możliwe, aby poprosić o wywnioskować typu wyrażenia:

Prelude> :t map 
map :: (a -> b) -> [a] -> [b] 

Wydaje się, że to trwa nazwy zmiennych typu z podpisem od map jest defined jak

map :: (a -> b) -> [a] -> [b] 
map _ []  = [] 
map f (x:xs) = f x : map f xs 

w Preludium. To ma sens! Moje pytanie brzmi: w jaki sposób są wybierane nazwy zmiennych typu, gdy nie ma podanego podpisu?

Przykładem może być

Prelude> :t map fst 
map fst :: [(b, b1)] -> [b] 

gdzie zbierane nazwy b i b1. To jasne, że musi nastąpić zmiana nazwy, ale po prostu zaczynając a, b ... dałby

map fst :: [(a, b)] -> [a] 

zamiast, który mi się znaleźć nieco bardziej czytelny.

Answer 1

Jak rozumiem, ghci wybiera nazwy w tej samej kolejności, w jakiej zawiera typy. Używa on schematu nazewnictwa, jak wspomniano, aby zdecydować o nazwie typu wyniku, czyli [b], ponieważ jest to nazwa typu określona w definicji map. Następnie decyduje, że funkcja będąca pierwszym parametrem dla map powinna również zwrócić coś typu b.

Pozostała zmienna typu, którą należy nazwać, jest zatem zmienną typu dla drugiego elementu w argumencie tuple na fst i ponownie analizuje definicję fst, aby zdecydować, której nazwy użyć. Definicja fst :: (a, b) -> a, czyli b byłaby tutaj preferowaną nazwą, ale ponieważ b jest już zajęta, dołącza ona 1, tak że staje się b1.

Myślę, że ten system ma zalety w sytuacjach, w których nie zajmuje się arbitralnymi typami, jak ma to miejsce w tym przypadku. Jeśli uzyskany typ wygląda mniej więcej tak, na przykład:

castAdd :: (Num n, Num n1, Num n2) => n -> n1 -> n2 

... to jest chyba bardziej czytelny niż:

castAdd :: (Num a, Num b, Num c) => a -> b -> c 

... bo można głównie polegać na tym n# oznacza numeryczny typ, ponieważ definicja klasy dla Num to class Num n where ....

EDYCJA: Tak, wiem, że castAdd jest niemożliwe do wdrożenia, ale jest to tylko przykład typu.