Was sind Typen mit Typabhängigkeiten?

"Qualifizierte Typen". Siehe Mark P. Jones. Qualifizierte Typen: Theorie und Praxis . Cambridge University Press, Cambridge, 1994.

Viele relevante Übereinstimmungen bei Google .

Typen mit dieser besonderen Art von Einschränkungen werden "qualifizierte Typen" genannt, und das Merkmal selbst wird manchmal als "qualifizierter Polymorphismus" bezeichnet. Ich glaube, die Terminologie wurde ursprünglich von Mark Jones 'ESOP '92-Papier eingeführt.

Qualifizierte Typen sollten nicht mit dem allgemeineren Begriff des "begrenzten Polymorphismus" verwechselt werden, auf dem Generika in Sprachen wie Java basieren. Bounded Polymorphism ist im Wesentlichen die (ziemlich komplizierte) Kombination von parametrischem Polymorphismus mit Subtyping, während qualifizierte Typen ohne Subtyping auskommen.

Ich bin kein Typentheorieexperte, aber mit ein wenig Nachforschung habe ich das gefunden (was vielleicht hilfreich ist oder nicht, aber ich kann das nicht in einen Kommentar einfügen).

Eine sanfte Einführung in Haskell: Klassen nennt den Num a -Teil den Kontext des Typs:

  

Die Einschränkung, dass ein Typ a eine Instanz der Klasse Eq sein muss, ist   geschriebene Gl. a. Somit ist Eq a kein Typusausdruck, sondern eher   drückt eine Einschränkung für einen Typ aus und wird als -Kontext bezeichnet.

Ich nehme an, Sie könnten sagen "ein Typ mit einem Kontext", oder wie Sie "Constrained Typ" erwähnt.

Ein anderer Ort, an dem Sie suchen können, ist, wo Typklassen zuerst (glaube ich) für Haskell beschrieben werden: Ad-hoc-Polymorphismus weniger ad-hoc machen [Nachsatz].

  

Typklassen scheinen eng mit den Problemen zu verwandt zu sein, die in   objektorientierte Programmierung, begrenzte Quantifizierung von Typen und   abstrakte Datentypen [CW85, MP85, Rey85]. Einige der Verbindungen sind   wie unten beschrieben, aber mehr Arbeit ist erforderlich, um diese zu verstehen   Beziehungen voll.

Dieses Papier wurde 1988 geschrieben, also bin ich mir nicht sicher, ob diese Beziehungen jetzt vollständig verstanden werden, aber die Wikipedia-Seite für beschränkt Quantifizierung erwähnt Haskell nicht, also bin ich mir nicht sicher, ob es genau dasselbe ist. (noch einmal kein Typentheoretiker - nur ein Typ, der Haskell mag)

Auch über den Typ square :: Num a => a -> a heißt es:

  

Dies wird gelesen, " square hat den Typ a -> a , für jeden a , so dass a gehört   zur Klasse Num (d. h., dass (+) , (*) und negate für a definiert sind). "

Man könnte sagen, der Typ "gehört zu einer Klasse".

Das ist alles, was ich habe. Persönlich denke ich, dass "eingeschränkte Typen" oder "Typen, die auf eine Klasse beschränkt sind" funktionieren.

Der Num a => -Teil wird tatsächlich als Einschränkung bezeichnet; Sie können es lesen als "wenn Num a wahr ist, dann ..."

Normalerweise werden Nebenbedingungen und Quantifizierer zusammen besprochen. Jeder eingeschränkte Typ kann in einen äquivalenten Typ konvertiert werden, in dem Constraints nur innerhalb von forall oder exists Quantoren angezeigt werden. Sie werden also nicht von "eingeschränkten Typen" so oft hören, wie Sie von "eingeschränkter parametrischer Polymorphie" ( forall a. C => T ), "eingeschränkten existentiellen Typen" ( exists a. C => T ) oder "eingeschränkter Polymorphie" (beide Arten von Quantifizierer).

Ein verwandter Begriff ist "beschränkter Polymorphismus". Bounded Polymorphism bedeutet in der Regel Constrained Polymorphism, wobei die Constraint ein Subtype oder Supertype Constraint ist. Diese Unterscheidung wird jedoch nicht strikt befolgt. In Sprachen mit Subtyping wie Java oder Scala, werden Sie oft jede Art von Constraint hören, die als "gebunden" bezeichnet wird.

Man könnte es einen begrenzten polymorphen Typ nennen (siehe Wikipedia ).