Warum muss fmap jedes Element einer Liste zuordnen?

Question

Nachdem das Buch Learn you a Haskell For Great Good und das sehr hilfreich Wiki Buch Artikel Haskell Category Theory lesen, die mich of confusing category objects with the programming objects, die gemeinsame Kategorie Fehler zu überwinden half ich habe immer noch die folgende Frage:

Warum muss fmap Karte über alle Elemente einer Liste?

Ich mag, dass es tut, ich möchte nur verstehen, wie dies theoretisch Kategorie gerechtfertigt ist. (Oder vielleicht ist es einfacher, mit HoTT zu rechtfertigen?)

In Scala Notation List ein Funktor ist, dass jede Art nimmt und Karten, die in eine Art aus der Menge aller Listentypen, zB es bildet den Typ Int auf die Typ List[Int] und ordnet die Funktionen auf Int zB

• Int.successor: Int => Int zu Functor[List].fmap(successor) : List[Int] => List[Int]
• Int.toString: Int => String zu Functor[List].fmap(toString): List[Int] => List[String]

Nun ist jede Instanz von List[X] ein Monoid mit einem empty function (mempty in Haskell) und combine function (mappend in Haskell). Meine Vermutung ist, dass man die Tatsache, dass Listen Monoids sind, verwenden kann, um zu zeigen, dass map alle Elemente einer Liste abbilden muss. Mein Gefühl hier ist, dass, wenn man die pure function from Applicative hinzufügt, dies uns eine Liste mit nur einem Element eines anderen Typs gibt. z.B. Applicative[List[Int]].pure(1) == List(1). Da map(succ) für diese Elemente die Singleton-Liste mit dem nächsten Element enthält, deckt dies alle diese Teilmengen ab. Dann nehme ich an, dass die Funktion combine auf all diesen Singletons uns alle anderen Elemente der Listen liefert. Irgendwie schränkt das die Art und Weise ein, wie die Karte funktionieren muss.

Ein weiteres suggestives Argument ist, dass map Funktionen zwischen Listen zuordnen muss. Da jedes Element in einer List[Int] vom Typ Int ist, und wenn man auf List[String] abbildet, muss man jedes Element davon abbilden, oder man würde nicht den richtigen Typ verwenden.

Also scheinen beide Argumente in die richtige Richtung zu zeigen. Aber ich fragte mich, was nötig war, um den Rest des Weges zu bekommen.

Gegenbeispiel?

Warum ist das keine Gegenbeispiel-Map-Funktion?

def map[X,Y](f: X=>Y)(l: List[X]): List[Y] = l match { 
    case Nil => Nil 
    case head::tail=> List(f(head)) 
} 

Es scheint, die Regeln

val l1 = List(3,2,1) 
val l2 = List(2,10,100) 

val plus2 = (x: Int) => x+ 2 
val plus5 = (x: Int) => x+5 

map(plus2)(List()) == List() 
map(plus2)(l1) == List(5) 
map(plus5)(l1) == List(8) 

map(plus2 compose plus5)(l1) == List(10) 
(map(plus2)_ compose map(plus5)_)(l1) == List(10) 

Ahh zu folgen. Aber es passt nicht zum id-Gesetz. Diese

def id[X](x: X): X = x 

map(id[Int] _)(l1) == List(3) 
id(l1) == List(3,2,1) 

Answer 1

stützt sich auf ein theoretisches Ergebnis als „Parametrizität“, die zuerst von Reynolds definiert und dann entwickelt von Wadler (unter anderem). Das vielleicht berühmteste Papier zu diesem Thema ist von Wadler.

Die Schlüsselidee ist, dass aus dem polymorphen Typ einer Funktion nur, können wir einige Informationen über die Semantik der Funktion erhalten.Zum Beispiel:

foo :: a -> a 

Von dieser Art allein, können wir das, wenn foo beendet sehen, es ist die Identitätsfunktion. Intuitiv kann foo nicht zwischen verschiedenen a s unterscheiden, da in Haskell z. Javas instanceof, die den tatsächlichen Laufzeittyp überprüfen können. In ähnlicher Weise

bar :: a -> b -> a 

muss das erste Argument zurückgeben. Und baz :: a -> a -> a muss entweder die erste oder die zweite zurückgeben. Und quz :: a -> (a -> a) -> a muss einige Male die Funktion auf das erste Argument anwenden. Sie haben wahrscheinlich jetzt die Idee.

Die allgemeine Eigenschaft, die aus einem Typ abgeleitet werden kann, ist ziemlich komplex, aber zum Glück kann es berechnet werden. In der Kategorientheorie hängt dies mit dem Begriff natural transformation zusammen.

Für den map Typen, erhalten wir die folgende beängstigend Eigenschaft:

forall t1,t2 in TYPES, f :: t1 -> t2. 
forall t3,t4 in TYPES, g :: t3 -> t4. 
    forall p :: t1 -> t3. 
    forall q :: t2 -> t4. 
    (forall x :: t1. g (p x) = q (f x)) 
    ==> (forall y :: [t1]. 
      map_{t3}_{t4} g (map2_{t1}_{t3} p y) = 
      map2_{t2}_{t4} q (map_{t1}_{t2} f y)) 

Oben, map ist die bekannte Kartenfunktion, während map2 jede beliebige Funktion ist, die (a -> b) -> [a] -> [b] hat eingeben.

Nehmen wir weiter an, dass map2 die Funktorgesetze erfüllt, insbesondere map2 id = id. Wir können dann p = id und t3 = t1 wählen. Wir bekommen

forall t1,t2 in TYPES, f :: t1 -> t2. 
forall t4 in TYPES, g :: t1 -> t4. 
    forall q :: t2 -> t4. 
    (forall x :: t1. g x = q (f x)) 
    ==> (forall y :: [t1]. 
      map_{t1}_{t4} g (map2_{t1}_{t1} id y) = 
      map2_{t2}_{t4} q (map_{t1}_{t2} f y)) 

Anwendung des Funktors Gesetz über map2:

forall t1,t2 in TYPES, f :: t1 -> t2. 
forall t4 in TYPES, g :: t1 -> t4. 
    forall q :: t2 -> t4. 
    (forall x :: t1. g x = q (f x)) 
    ==> (forall y :: [t1]. 
      map_{t1}_{t4} g y = 
      map2_{t2}_{t4} q (map_{t1}_{t2} f y)) 

Nun lassen Sie uns wählen t2 = t1 und f = id:

forall t1 in TYPES. 
forall t4 in TYPES, g :: t1 -> t4. 
    forall q :: t1 -> t4. 
    (forall x :: t1. g x = q x) 
    ==> (forall y :: [t1]. 
      map_{t1}_{t4} g y = 
      map2_{t1}_{t4} q (map_{t1}_{t1} id y)) 

Durch die Funktors Gesetz map:

forall t1, t4 in TYPES. 
    forall g :: t1 -> t4, q :: t1 -> t4. 
    g = q 
    ==> (forall y :: [t1]. 
      map_{t1}_{t4} g y = 
      map2_{t1}_{t4} q y) 

die

forall t1, t4 in TYPES. 
forall g :: t1 -> t4. 
    (forall y :: [t1]. 
      map_{t1}_{t4} g y = 
      map2_{t1}_{t4} g y) 

bedeutet die

forall t1, t4 in TYPES. 
      map_{t1}_{t4} = map2_{t1}_{t4} 

Zusammengefasst bedeutet:

Wenn map2 jede Funktion mit polymorphen Typ ist (a -> b) -> [a] -> [b], und so, dass sie das erste Funktors Gesetz map2 id = id erfüllt, dann map2 muss der Standardfunktion map entsprechen.

Siehe auch eine related blog post by Edward Kmett.

Beachten Sie, dass das obige in Scala nur gilt, wenn Sie x.isInstanceOf[] und andere Reflektionswerkzeuge nicht verwenden, die die Parameterik brechen können.