Kind vs Rank in type theory

Question

Ciężko mi zrozumieć typy Higher Kind vs Higher Rank. Rodzaj jest dość prosty (dzięki temu, że Haskell do tego pisze) i myślałem, że ranga jest jak rodzaj, gdy mówimy o typach, ale najwyraźniej nie! Przeczytałem artykuł z Wikipedii bezskutecznie. Czy ktoś może wyjaśnić, czym jest ranga? i co oznacza wyższa ranga? Polimorfizm wyższej rangi? jak to przychodzi do Rodzin (jeśli w ogóle)? Porównanie Scali z Haskellem też byłoby niesamowite.

Answer 1

Pojęcie rangi nie jest tak naprawdę związane z pojęciem rodzaju.

Ranga systemu typu polimorficznego opisuje, gdzie mogą pojawiać się typy forall. W systemie o typie rank-1 mogą pojawiać się tylko na najbardziej zewnętrznym poziomie, w systemie typu rank-2 mogą pojawiać się na jednym poziomie zagnieżdżania i tak dalej.

Na przykład forall a. Show a => (a -> String) -> a -> String byłby typem rank-1, a forall a. Show a => (forall b. Show b => b -> String) -> a -> String byłby typem rank-2. Różnica między tymi dwoma typami polega na tym, że pierwszym argumentem funkcji może być dowolna funkcja pobierająca jeden argument i zwracająca łańcuch. Tak więc funkcja typu Int -> String byłaby poprawnym pierwszym argumentem (podobnie jak hipotetyczna funkcja intToString), tak samo jak funkcja typu forall a. Show a => a -> String (jak show). W drugim przypadku tylko funkcja typu forall a. Show a => a -> String byłaby prawidłowym argumentem, tj. show byłaby w porządku, ale nie byłaby to intToString. W konsekwencji następująca funkcja byłaby funkcja prawną drugiego typu, ale nie pierwszy (gdzie ++ ma reprezentować konkatenacji String):

higherRankedFunction(f, x) = f("hello") ++ f(x) ++ f(42) 

Zauważ, że tutaj funkcja f nakłada się (potencjalnie) trzy różne typy argumentów. Więc jeśli f byłaby funkcją intToString, to by nie działało.

Zarówno Haskell, jak i Scala są Rangami 1 (więc powyższa funkcja nie może być zapisana w tych językach) domyślnie. Ale GHC zawiera rozszerzenie językowe, aby umożliwić polimorfizm Rank-2, a inne, aby umożliwić polimorfizm Rank-n dla arbitralnego n.