2016-01-26 17 views
18

konnte ich Functor Definition aus der Kategorie Theorie Haskell Definition in der folgenden Art und Weise abzubilden: da Objekte von Hask Typen sind, die Funktors FWas ist Applicative Functor Definition aus der Kategorie Theorie POV?

  • F a durch jede Art a von Hask in den neuen Typ abbildet, grob Sprichwort, "F" davor.
  • Karten jeden Morphismus a -> b von Hask zu dem neuen Morphismus F a -> F b mit fmap :: (a -> b) -> (f a -> f b).

So weit, so gut. Jetzt komme ich an die Applicative und kann in Lehrbüchern kein solches Konzept finden. Wenn ich mir anschaue, was es zu Functor, ap :: f (a -> b) -> f a -> f b hinzufügt, habe ich versucht, eine eigene Definition zu finden.

Zuerst bemerkte ich, dass seit (->) auch ein Typ ist, Morphismen von Hask sind Objekte davon auch. Vor diesem Hintergrund habe ich einen Vorschlag gemacht, dass der anwendungsbezogene Funktor ein Funktor ist, der auch "Pfeil" -Objekte der Quellkategorie in Morphismen der Zielkategorie einordnen kann.

Ist das eine richtige Intuition? Können Sie eine formellere und strengere Definition geben?

+1

http://cstheory.stackexchange.com/questions/12412/explaining-applicative-functor-in-categorical-terms-monoidal-functors –

Antwort

25

Der Schlüssel zum Verständnis applicative functors definieren ist herauszufinden, welche Struktur sie bewahren.

Reguläre Funktoren bewahren die grundlegende kategorische Struktur: Sie ordnen Objekte und Morphismen zwischen Kategorien zu und bewahren die Gesetze der Kategorie (Assoziativität und Identität).

Aber eine Kategorie kann mehr Struktur haben. Zum Beispiel kann es die Definition von Abbildungen ermöglichen, die wie Morphismen sind, aber mehrere Argumente annehmen. Solche Zuordnungen werden durch Curry definiert: z. B. wird eine Funktion von zwei Argumenten als eine Funktion eines Arguments definiert, das eine andere Funktion zurückgibt. Dies ist möglich, wenn Sie ein Objekt definieren können, das einen Funktionstyp darstellt. Im Allgemeinen wird dieses Objekt als Exponential bezeichnet (in Haskell ist es nur der Typ b->c). Wir können dann Morphismen von einem Objekt zu einer Exponentialfunktion haben und sie als zweiargumentalen Morphismus bezeichnen.

Die traditionelle Definition eines anwendungsbezogenen Funktors in Haskell basiert auf der Idee, Funktionen mehrerer Argumente abzubilden. Aber es gibt eine äquivalente Definition, die die Multi-Argument-Funktion entlang einer anderen Grenze aufteilt. Sie können eine solche Funktion als ein Mapping von einem Produkt (ein Paar, in Haskell) auf einen anderen Typ (hier, c) betrachten.

Das erlaubt uns, anwendungsbezogene Funktoren als Funktoren zu betrachten, die das Produkt bewahren. Ein Produkt ist jedoch nur ein Beispiel für eine so genannte monoidale Struktur.

Im Allgemeinen ist eine monoidale Kategorie eine Kategorie, die mit einem Tensorprodukt und einem Einheitsobjekt ausgestattet ist. In Haskell könnte dies beispielsweise das kartesische Produkt (ein Paar) und der Einheitstyp () sein. Beachten Sie jedoch, dass die monoiden Gesetze (Assoziativität und Einheitsgesetze) nur bis zu einem Isomorphismus gültig sind. Zum Beispiel:

(a,()) ~ a 

Ein applikativer Funktor könnte dann als ein Funktor definiert werden, der die monoidale Struktur beibehält. Insbesondere sollte es die Einheit und das Produkt erhalten. Es sollte egal sein, ob wir die "Multiplikation" vor oder nach der Anwendung des Funktors durchführen. Die Ergebnisse sollten isomorph sein.

Allerdings brauchen wir nicht wirklich einen vollwertigen monoidalen Funktor. Wir brauchen nur zwei Morphismen (im Gegensatz zu Isomorphismen) - einen für die Multiplikation und einen für die Einheit. Ein solcher Funktor, der die monoidale Struktur halb konserviert, wird als laxer monoidaler Funktor bezeichnet. Daraus ergibt sich die alternative Definition:

class Functor f => Monoidal f where 
    unit :: f() 
    (**) :: f a -> f b -> f (a, b) 

Es ist leicht zu zeigen, dass Monoidal zu Applicative entspricht.

pure x = fmap (const x) unit 
unit = pure() 

Die applicative Gesetze folgen einfach aus der Erhaltung der Monoid Gesetze (Assoziativität und Einheit Gesetz): Zum Beispiel können wir pure von unit und umgekehrt erhalten.

In der Kategorie der Theorie, Erhaltung der monoidal Struktur ist im Zusammenhang mit tensorielle Stärke, so dass ein applicative Funktors auch als starke lasche monoidal Funktors bekannt ist. In Hask hat jedoch jeder Funktor kanonische Stärke in Bezug auf das Produkt, so dass diese Eigenschaft der Definition nichts hinzufügt.

Nun, wenn Sie vertraut sind mit der Definition einer Monade als Monoid in der Kategorie der endofunctors, könnten Sie interessiert sein zu wissen, dass die Anwendung in ähnlicher Weise Monoide in der Kategorie der endofunctors sind, wo das Tensor Produkt ist Tag Windung. Aber das ist viel schwerer zu erklären.

+0

Was ist das Zeug "Stärke"? – dfeuer

+0

Ja, wenn Sie etwas hinzufügen können, was "Stärke" hier bedeutet, würde es klären; vor allem, da Linksroundouts Antwort Links zu https://en.wikipedia.org/wiki/Monoidal_functor enthält, die "starke monoidale Funktoren" zu definieren scheinen, um "monoides Funktor mit einigen angenommenen Einschränkungen" und "laxe monoidale Funktoren" zu bedeuten, "keine zusätzlichen Annahmen" ", so scheint in dieser Terminologie" starker laxer monoidaler Funktor "keinen Sinn zu ergeben. – Ben

+5

Ich persönlich bevorzuge es, anwendungsbezogene Funktoren eher als geschlossene Funktoren denn als monoidale Funktoren zu betrachten. Die Tatsache, dass sie monoidal sind, ist mehr oder weniger zufällig und wird durch die Erhaltung von Exponentialen erzwungen, weshalb sich die "monoidale" Kodierung von Dingen so unordentlich anfühlt, während die (<*>) :: f (a -> b) - > fa -> fb' Kombinator, den wir verwenden, ist genau die Abbildung von Exponentialen! Eine andere Möglichkeit, über einen Applicative nachzudenken, ist ein monoides Objekt in Bezug auf die (kovariante) Day-Faltung.Diese Ansicht hat den Vorteil, dass sie den Weg zum Finden einer kontravarianten Form von Applicative beleuchtet. –

11

Sie haben recht, Applicative übersetzt weniger einfach als Functor oder Monad. Aber im Grunde ist es die Klasse der monoidal functors:

class Functor f => Monoidal f where 
    pureUnit :: f() 
    fzip :: f a -> f b -> f (a,b) 

Von dass Sie – innerhalb Hask

pure x = fmap (const x) pureUnit 

und

fs <*> xs = fmap (uncurry ($)) $ fzip fs xs