Warum sollte / sollte nichts darauf abstellen, dass s isomorph zu t ist und b isomorph zu a in einer Isomorphie vom Typ Iso s t a b ?
Ich verstehe, dass wir eine Vorwärtszuordnung s -> a und eine Rückwärtszuordnung b -> t haben, aber warum ist diesen Zuordnungen in
Was Sie isomorph machen möchten, ist nicht s bis t oder a bis b , sondern stattdessen s bis a und t bis b . Betrachten Sie das Beispiel:
Hier stellen wir die Iso swapped mit der Lens _1 zusammen; In dieser Verwendung entspricht ihre Zusammensetzung der Lens _2 , und so wird show auf das zweite Element des Tupels (True, ()) angewendet. Beachten Sie, dass show den Typ ändert. Also, um welchen Typ benutzen wir eigentlich Iso swapped hier?
s ist der Typ unseres ursprünglichen Tupels, (Bool, ())
t ist der Typ des Endergebnisses, (Bool, String)
a ist der Typ von s nach dem Austausch, ((), Bool)
b ist der Typ von t vor dem Zurücktauschen, (String, Bool)
Mit anderen Worten verwenden wir swapped am Typ
Jede der Abbildungen s -> a und b -> t ist eine Bijektion, aber es gibt keine solche notwendige Beziehung zwischen den anderen Typen.
Warum gibt es keine aufgelisteten Gesetze für Iso s, die sagen, dass dies Bijektionen sein müssen, weiß ich nicht.
EDIT: Der Abschnitt "Warum ist es eine Objektivfamilie?" in dem Link, der von @bennofs in den obigen Kommentaren gepostet wurde, hat einige Dinge für mich geklärt. Offensichtlich beabsichtigt Edward Kmett, dass diese Typen nicht völlig frei variieren können.
Obwohl es in den Typen einer Optik nicht direkt ausgedrückt werden kann, ohne dass es umständlich ist, sie zu verwenden,
Die Absicht ist, dass eine typändernde Optikfamilie ( Lens , Iso oder andere) Typen haben sollte, die durch die Typfamilien inner und outer gegeben sind. Wenn einer der Typen von Iso
Dann sollte es zwei Indextypen geben: i und j , so dass
Außerdem dürfen Sie i und j tauschen, und obwohl dies nicht automatisch durchgesetzt wird, sollte das Ergebnis noch für Ihre polymorphe Iso legal sein. I.e. Sie sollten auch anIso am Typ
Das gilt eindeutig für swapped . Beides sind legale Typen dafür:
Mit anderen Worten: Wenn eine polymorphe Iso -Familie typenverändernd ist, muss auch die umgekehrte -Typänderung unterstützt werden. (Auch zusammengesetzte Typänderungen. Ich rieche hier eine natürliche Verwandlung aus der Kategorientheorie, was meiner Meinung nach auch eine Art ist, wie Kmett daran denkt.)
Beachten Sie auch, dass wenn Sie eine polymorphe Iso als
Damit dies auch den Typ iso f g :: Iso t s a b hat, müssen f und g ebenfalls die Typen
Beachten Sie, dass f , das am ersten Typ s -> a verwendet wird, den richtigen Typ hat, der die Umkehrung von g ist, der an seinem zweiten Typ a -> s verwendet wird, und umgekehrt.
Für ein konkretes Beispiel ist swapped hier ein wenig schlecht, da seine f und g , die für Tupel verwendet werden, identisch sind, im Wesentlichen sind sie beide \(x,y) -> (y,x) , was eine eigene Umkehrung ist. Und das beste andere nicht Simple Beispiel, das ich in Control.Lens.Iso sehe, ist curried , was etwas zu kompliziert erscheint, um es zu klären.