Bedeutung von "positiver Position" und "negativer Position" in der Typentheorie?

Was bedeutet "in positiver Position" und "in negativer Position" im Kontext der Typentheorie?

Das einzige, was ich aus Bob Harpers Blogbeitrag zu diesem Thema verstanden habe, ist, dass es einen Zusammenhang zwischen Polarität in diesem Sinne in der Typentheorie und Polarität in der Logik gibt, aber ich weiß nicht, was dieser Zusammenhang ist.

Leider ist "Polarität" in der Typentheorie ein etwas überladenes Konzept. "Positive Position" und "negative Position" beziehen sich auf einen anderen Begriff der Polarität als das, worüber Bob mit Fokussierung / Polarisation spricht.

Deine Bedeutung

Wenn Sie einen induktiven Typ definieren, geben Sie eine Reihe von Regeln an, die Operationen für den von Ihnen definierten Typ entsprechen. Zum Beispiel könnte man sagen, dass a Natetwas mit ist

• ein Wert zero : Nat
• eine Funktion suc : Nat -> Nat

Und dann erwarten Sie, dass Natalle Werte enthalten sind, die durch wiederholtes Anwenden sucauf andere Nats und Includes generiert werden können zero. In Übereinstimmung mit dieser induktiven Konstruktion erhalten wir ein Rekursionsprinzip über Nats, das auf der Tatsache basiert, dass jedes Natvon diesen Konstruktoren erzeugt wird.

rec : A -> (A -> A) -> Nat -> A

damit

rec Z S zero = zero
rec Z S (suc n) = S (rec Z S n)

Es gibt jedoch einige Einschränkungen, was wir als Regeln schreiben können. Andernfalls können wir eine Reihe von Regeln aufschreiben, für die das Rekursionsprinzip nicht gerechtfertigt werden kann. Betrachten Sie den "induktiven Typ" Dmit einem Konstruktor

• d : (D -> D) -> D

Hier gibt es hier kein vernünftiges Rekursionsprinzip. und das aus gutem grund! Wenn wir ein Rekursionsprinzip hätten, könnten wir es verwenden, um eine Version der Selbstanwendung und damit die Nichtterminierung zu codieren. Dies bedeutet, dass Des nicht als "induktiv" bezeichnet werden kann, da induktive Typen endliche Konstruktionen sind, die durch wiederholtes Anwenden von Konstruktoren erzeugt werden!

Um damit umzugehen, beschränken wir, wie induktive Typen in der Typentheorie rekursiv sein können. Insbesondere verhindern wir, dass sie an "negativen Stellen" erscheinen. Dies ist der Begriff der Polarität, über den Sie gesprochen haben. Die Polarität einer Position wird somit bestimmt,

1. Das Argument beginnt in einer positiven Position
2. Jedes Mal, wenn wir einen Pfeil nach links gehen, wechselt die Polarität

So Xist positiv in den ersten beiden und negativ in den zweiten beiden

X
Int -> X
X -> Int
(Unit -> X) -> Int

Diese Idee ist mit einem Rückgriff auf die Kategorietheorie gerechtfertigt, bei der aus einem induktiven Typ, dessen einzige Rezidive positiv sind, ein kovarianter Funktor entsteht. Die Details, wie das funktioniert und warum es interessant ist, sind ein bisschen lang.

Bob Harpers Bedeutung

In seinem Blogpost sprach Harper über eine andere Bedeutung von Polarität. Diese Polarität bezieht sich darauf, wie verschiedenen Konnektiven in der Logik Bedeutung gegeben wird. Insbesondere können wir Konnektive auf zwei Arten klassifizieren

• Positive Konnektive können definiert werden, indem definiert wird, wie sie eingeführt werden sollen (ihre Einführungsregeln).
• Negative Konnektive können definiert werden, indem definiert wird, wie sie verwendet werden (ihre Eliminierungsregeln).

In Bezug auf die Programmiersprache erfasst dies die Unterscheidung zwischen faulen und strengen Typen. Ein strikter Typ wird durch seine Werte definiert. Ein Fauler wird dadurch definiert, wie Muster auf ihnen übereinstimmen können. Um dies richtig zu handhaben, definieren wir eine Sprache mit zwei Hauptkonstrukten, Möglichkeiten zum Aufbau positiver Typen und "Stacheln" zum Zerlegen negativer Typen. Wir können dies verwenden, um sowohl strenge als auch faule Berechnungen in eine Sprache zu integrieren.

Um dies besser zu verstehen, verweise ich Sie auf Kapitel 38 von Bob Harpers Buch .