Kind vs Rank in der Typentheorie

Question

Ich habe eine schwere Zeit, Höherer Typ vs Höherer Rang zu verstehen. Kind ist ziemlich einfach (danke Haskell Literatur dafür) und ich dachte, Rang ist wie freundlich, wenn man über Typen spricht, aber anscheinend nicht! Ich habe den Wikipedia-Artikel vergeblich gelesen. Kann mir bitte jemand erklären, was ein Rank ist? und was ist mit Höherem Rang gemeint? Höherer Polymorphismus? wie kommt das zu Kinds (wenn überhaupt)? Vergleichen Scala und Haskell wäre auch super.

Answer 1

Das Konzept des Rangs ist nicht wirklich mit dem Begriff der Arten verwandt.

Der Rang eines Systems vom polymorphen Typ beschreibt, wo forall s in Typen auftreten können. In einem System des Rang-1-Typs forall kann s nur auf der äußersten Ebene erscheinen, in einem System des Rang-2-Typs können sie auf einer Ebene der Verschachtelung erscheinen und so weiter.

Also zum Beispiel forall a. Show a => (a -> String) -> a -> String wäre ein Rang-1-Typ und forall a. Show a => (forall b. Show b => b -> String) -> a -> String wäre ein Rang-2-Typ. Der Unterschied zwischen diesen beiden Typen besteht darin, dass im ersten Fall das erste Argument für die Funktion jede Funktion sein kann, die ein darstellbares Argument annimmt und einen String zurückgibt. Eine Funktion vom Typ Int -> String wäre also ein gültiges erstes Argument (wie eine hypothetische Funktion intToString), also eine Funktion vom Typ forall a. Show a => a -> String (wie show). Im zweiten Fall wäre nur eine Funktion vom Typ forall a. Show a => a -> String ein gültiges Argument, d. H. show wäre in Ordnung, aber intToString wäre nicht gültig. Als Folge würde die folgende Funktion eine juristische Funktion des zweiten Typs, aber nicht die erste (wo ++ soll String-Verkettung darzustellen):

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

Beachten Sie, dass hier die Funktion f angewendet wird (potentiell) drei verschiedene Arten von Argumenten. Wenn also f die Funktion intToString wäre, würde das nicht funktionieren.

Sowohl Haskell als auch Scala sind standardmäßig Rank-1 (daher kann die obige Funktion nicht in diesen Sprachen geschrieben werden). Aber GHC enthält eine Spracherweiterung, um Rang-2-Polymorphismus zu ermöglichen, und eine andere, um Rank-n-Polymorphismus für beliebiges n zu ermöglichen.