Was bedeutet das Naturgesetz für Traversables?

Das Naturgesetz besagt:

t . traverse f == traverse (t . f) -- for every applicative transformer t

Wenn nun für die RHS des Gesetzes f den Typ hat Applicative a => x -> a y, muss t (Applicative a, Applicative b) => a y -> b yaufgrund der Funktionszusammensetzung vom Typ sein .

Für die LHS hat die Traverse f den Typ (Applicative a, Traversable c) => c x -> a (c y). Da aber die Traverse f mit t zusammengesetzt ist. Traverse f, t muss vom Typ (cx -> a (cy)) -> b y sein.

Nun hat t für die LHS den Typ a (cy) -> by, aber von der RHS hat es den Typ ay -> b y. Wie klingt das Gesetz aus einer Typperspektive?

Bearbeiten: Der Typ t in LHS wurde korrigiert

Ich denke, was Sie verpasst haben, ist, dass tes sich um eine natürliche Transformation handeln soll (die wahrscheinlich auch einige strukturerhaltende Eigenschaften haben muss). Natürliche Transformationen werden wie folgt quantifiziert:

t :: forall z. a z -> b z   -- "t is an N.T. from a ~> b"

Rechts instanziieren wir es y, um zu bekommen t :: a y -> b y; links instanziieren wir es um c yzu bekommen a (c y) -> b (c y). Ich denke, dass eine natürliche Transformation die äußere Schicht verändert, egal was sich darin befindet. Naturgesetze sprechen immer über Beziehungen zwischen den verschiedenen Arten, wie etwas instanziiert wird.

t                :: forall z. a z -> b z

f                :: x -> a y
t                :: a y -> b y           -- instantiated at y
t . f            :: x -> b y
traverse (t . f) :: c x -> b (c y)

traverse f       :: c x -> a (c y)
t                :: a (c y) -> b (c y)   -- instantiated at (c y)
t . traverse f   :: c x -> b (c y)