könnte jemand die Verbindung zwischen Typ Kovarianz / Kontra und Kategorientheorie erklären?

StackOverflow https://stackoverflow.com/questions/3125409

Frage

Ich beginne gerade über Kategorientheorie zu lesen, und würde es sehr schätzen, wenn jemand die Verbindung zwischen CS Kontra / Kovarianz und Kategorientheorie erklären könnte. Was wären einige Beispiel Kategorien (das heißt, was ihre Objekte / morphisms?)? Vielen Dank im Voraus?

War es hilfreich?

Lösung

Ein kontra Funktors von $ C $ bis $ D $ ist genau das gleiche wie ein normales (dh covariant) Funktor von $ C $ bis $ D ^ {op} $, wobei $ D ^ {op} $ das ist gegenüber Kategorie von $ D $. So ist es wahrscheinlich am besten zuerst entgegengesetzte Kategorien zu verstehen - dann werden Sie automatisch kontra functors verstehen

kontra functors nicht kommen alle, die oft in CS, obwohl ich von zwei Ausnahmen denken kann:

  1. Sie können von Kontra im Zusammenhang mit Subtyping gehört. Obwohl dies technisch der Begriff ist, ist die Verbindung wirklich, wirklich schwach. In der objektorientierten Programmierung, bilden die Klassen eine partielle Ordnung; jeder Teilauftrag ist eine Kategorie mit "binary hom-Sets" - gegeben zwei beliebige $ A $ und $ B $ Objekte, gibt es genau einen Morphismus $ A \ to B $ iff $ A \ leq B $ (beachten Sie die Richtung; diese etwas verwirrende Orientierung ist der Standard aus Gründen, die ich hier nicht erklären) und keine morphisms sonst.

    Parameterized Typen wie, sagen wir, Scala Partielle Funktion [-A, Einheit] functors von dieser einfachen Kategorie selbst sind ... wir in der Regel auf das konzentrieren, was sie zu Objekten zu tun: Da eine Klasse X, Partielle Funktion [X, Einheit] ist auch eine Klasse. Aber functors bewahren morphisms auch; in diesem Fall, wenn wir eine Unterklasse Hund von Tiere hätten, würden wir ein Morphismus Hund $ \ bis $ Tier haben, und der Funktors würde dieses morphism bewahren, uns eine morphism Partielle Funktion [Tier, Einheit] $ \ to $ Partielle Funktion [Hund zu geben, Einheit], uns zu sagen, dass Partielle Funktion [Tier, Einheit] ist eine Unterklasse von Partielle Funktion [Hund, Einheit]. Wenn Sie darüber nachdenken, ist es sinnvoll: Angenommen, Sie eine Situation, wo Sie eine Funktion benötigen, die auf Hunde funktioniert. Eine Funktion, die funktioniert auf allen Tieren sicher funktionieren würde, da!

    sagte, dass unter Verwendung von Voll auf Kategorie Theorie zu sprechen über teilweise geordnete Mengen große Zeit viel des Guten ist.

  2. Weniger häufig, aber tatsächlich verwendet die Theorie der Kategorie: die Kategorie-Typen (Hask) betrachten, deren Objekte sind die Arten der Programmiersprache Haskell und wo ein Morphismus $ \ tau_1 \ to \ tau_2 $ ist eine Funktion des Typs $ \ tau_1 $ -> $ \ tau_2 $. Es gibt auch eine Kategorie Urteile (Hask), deren Objekte sind Listen von Typisierung Urteile \ $ tau_1 \ vdash \ tau_2 $ und deren Morphismen sind Beweise aller Urteile auf einer Liste, die die Urteile auf der anderen Liste als Hypothesen verwenden. Es gibt einen Funktor von Typen (Hask) auf Urteile (Hask), die einen Typen (Hask) nimmt -morphism $ f: A \ to B $ zum Beweis 

     B |- Int
    ----------
      ......
    ----------
     A |- Int

, die ein Morphismus $ (B \ vdash Int) \ (A \ vdash Int) $ - Bekanntmachung der Richtungsänderung. Im Grunde, was das sagt, ist, dass, wenn Sie eine Funktion haben, die dann auch A die in B'a und einen Ausdruck des Typs Int mit einer freien Variable x vom Typ B, dann können Sie es wickeln mit „let x = fy in. ..“und nach wie vor vom Typ Int bei einem Ausdruck kommen, aber deren einzige freie Variable ist vom Typ $ A $, $ B $ nicht.

Lizenziert unter: CC-BY-SA mit Zuschreibung
Nicht verbunden mit StackOverflow
scroll top