2016-03-21 2 views
0

Selon Control.Foldl documentation:Pourquoi tout Lens correspond-il au type Foldl.Handler?

Toute lentille, traversal ou prisme tapera vérifier en tant que gestionnaire

type Handler a b 
    = forall x. (b -> Constant (Endo x) b) -> a -> Constant (Endo x) a 

On pourrait prétendre que, puisque l'objectif permet une Functor qui n'est pas Constant seul le sous-ensemble de l'objectif doit vérifier le type. Pourquoi cette déclaration est-elle incorrecte?

Répondre

5

Vous avez vos directions mélangées, c'est tout. Les optiques qui y sont décrites sont de la forme

type Foo s t a b = forall f. SomeConstraints f => (a -> f b)-> (s -> f t) 

Petit FIB, pour prismes il est censé fonctionner avec un Choice arbitraire profunctor, mais -> est une sorte de l'exemple canonique d'une telle structure afin que nous puissions spécialiser les prismes pour travailler uniquement à travers ces profuncteurs. La raison pour laquelle ce processus est légal est identique à ce que nous allons faire avec f afin de suspendre l'incrédulité pendant une minute et lire

Maintenant, si nous instancions s et t comme a et a et b comme b nous obtenir

forall f. SomeConstraints f => (b -> f b) -> (a -> f a) 

maintenant, cela signifie que si nous avons une certaine optique, comme une lentille, prisme ou traversal, nous pouvons instancier ses paramètres de type de sorte qu'il est presque sous la forme d'un Handler. La seule différence est la nôtre est garanti de travailler pour tout f à condition qu'il satisfasse les contraintes que nous avons choisies. Si nous savons que Constant (Endo x) satisfait à ces contraintes, alors nous pouvons spécialiser silencieusement cette optique pour travailler seulement avec f. C'est juste une vieille instanciation polymorphe! Et puisque Constant a est un Functor et un Applicative il fonctionnera avec n'importe quel objectif ou traversal. Ce sous-typage et instanciation implicite est au cœur du fonctionnement de l'ensemble de lentilles, en laissant transparentes toutes ces choses. Haskell mélangeons et associons les abstractions et il s'installera automatiquement sur la "plus grande limite inférieure" de l'ensemble des optiques en utilisant.

Le tout se résume au fait que dans Haskell, si nous avons e :: forall t. T, alors pour tout tau correctement lié, nous avons aussi e :: [tau/t]T. Il y a quelques plis une fois que nous jetons dans les contraintes de type mais dans l'ensemble, c'est tout simplement le fait que l'application de type est silencieuse par défaut dans Haskell.