haskell - ¿No es redundante para Control.Lens.Setter envolver tipos en functores?

applicative lenses (2)

Estoy viendo el video introducción de Control.Lens .
Me pregunto por qué es necesario que el tipo Setter envuelva las cosas en los funtores.
Se define (aproximadamente) de esta manera:

type Control.Lens.Setter s t a b = (Functor f) => (a -> f a) -> s -> f t

Digamos que tengo un dato llamado Point que se define así:

data Point = Point { _x :: Int, _y :: Int } deriving Show

Entonces puedo escribir mis propios xlens así:

type MySetter s t a b = (a -> b) -> s -> t xlens :: MySetter Point Point Int Int xlens f p = p { _x = f (_x p) }

Y puedo usarlo así:

p = Point 100 200 xlens (+1) p -- Results in Point { _x = 101, _y = 200 }

Al usar Control.Lens , el mismo efecto se logra al:

over x (+1) p

donde se encuentra lo siguiente:

x :: Functor f => (Int -> f Int) -> Point -> f Point over :: Setter Point Point Int Int -> (Int -> Int) -> Point -> Point

Así que mi pregunta es, ya que el mismo efecto se puede lograr de una manera más simple, ¿por qué Control.Lens envuelve las cosas en los funtores? A mi me parece redundante, ya que mi xlens hace lo mismo que Control.Lens ''s over x .

Solo para el registro, también puedo encadenar mis lentes de la misma manera:

data Atom = Atom { _element :: String, _pos :: Point } deriving Show poslens :: MySetter Atom Atom Point Point poslens f a = a { _pos = f (_pos a) } a = Atom "Oxygen" p (poslens . xlens) :: (Int -> Int) -> Atom -> Atom (poslens . xlens) (+1) a -- Results in Atom "Oxygen" (Point 101 200)

En cierto sentido, la razón por la que la lens envuelve a los instaladores en functor-return es que de lo contrario serían demasiado poderosos .

De hecho, cuando se utiliza un definidor, el funtor se creará una instancia de Identity todos modos, que es exactamente igual que su firma propuesta. Sin embargo, la implementación de un setter no debe explotar este hecho . Con tu firma, podría escribir algo como

zlens :: MySetter Point Point Int Int zlens _f p = p -- no z here!

Bueno, esto simplemente no es posible con la firma basada en Functor , ya que los zlens necesitarían ser cuantificados universalmente sobre el functor, no podría saber cómo inyectar un resultado en la envoltura f . ¡La única manera de obtener un resultado del tipo de functor es aplicar primero la función de establecimiento a un campo del tipo correcto!

Entonces, esto es solo un buen teorema libre ^† .

Más prácticamente, necesitamos el envoltorio functor para la compatibilidad . Si bien puede definir definidores sin esta envoltura, esto no es posible para quienes los obtienen, ya que estos usan Const lugar de Identity , y necesitan el polimorfismo agregado en el primer argumento de este tipo de constructor. Al requerir un envoltorio de este tipo para todos los sabores de lentes (solo con diferentes restricciones de clase), podemos usar los mismos combinadores para todos ellos, sin embargo, el sistema de tipos siempre colapsará la funcionalidad según las características que sean realmente aplicables a la situación.

^† _{Pensándolo bien, la garantía en realidad no es muy fuerte ... Todavía puedo subvertirla con un poco de valor de fmap (const old) , pero ciertamente no es algo que pueda ocurrir de manera realista por error.}

Esta es una pregunta maravillosa y requerirá un poco de desempaque.

Quiero corregirlo suavemente en un punto desde el principio: el tipo de Setter en el paquete de lens partir de las versiones recientes es

type Setter s t a b = (a -> Identity b) -> s -> Identity t

Sin Functor a la vista ... todavía.

Eso no invalida tu pregunta sin embargo. ¿Por qué no es el tipo simplemente

type Setter s t a b = (a -> b) -> s -> t

Para eso primero tenemos que hablar de Lens .

Lente

Una Lens es un tipo que nos permite realizar operaciones de captador y configurador. Estos dos combinados forman una hermosa referencia funcional.

Una selección simple para el tipo de Lens es:

type Getter s a = s -> a type Setter s t a b = (a -> b) -> s -> t type Lens s t a b = (Getter s a, Setter s t a b)

Sin embargo, este tipo es profundamente insatisfactorio.

No logra componer con . , que es quizás el mejor punto de venta del paquete de lens .
Es más bien ineficiente en memoria construir muchas tuplas, solo para separarlas más tarde.
El grande: las funciones que aceptan captadores (como view ) y setters (como over ) no pueden usar lentes porque sus tipos son muy diferentes.

Sin el último problema resuelto, ¿por qué molestarse en escribir una biblioteca? No nos gustaría que los usuarios tuvieran que pensar constantemente en dónde se encuentran en la jerarquía de UML de la óptica, ajustando sus llamadas de función cada vez que se mueven hacia arriba o hacia abajo.

La pregunta del momento es entonces: ¿hay un tipo que podamos escribir para Lens que sea automáticamente un Getter y un Setter ? Y para eso tenemos que transformar los tipos de Getter y Setter .

Adquiridor

Primero note que s -> a es equivalente a forall r. (a -> r) -> s -> r forall r. (a -> r) -> s -> r . Esta transformación en estilo de paso de continuación está lejos de ser evidente. Es posible que pueda intuir esta transformación de la siguiente manera: "Una función de tipo s -> a es una promesa que, dado cualquier s me puede entregar una a . Pero eso debería ser equivalente a la promesa que se le da a una función que se asigna a a r me puede entregar una función que mapea de s a r también ". ¿Tal vez? Tal vez no. Puede haber un salto de fe involucrado aquí.
Ahora defina newtype Const ra = Const r deriving Functor . Tenga en cuenta que Const ra es el mismo que r , matemáticamente y en tiempo de ejecución.
Ahora note que type Getter sa = forall r. (a -> r) -> s -> r type Getter sa = forall r. (a -> r) -> s -> r se puede reescribir como type Getter stab = forall r. (a -> Const rb) -> s -> Const rt type Getter stab = forall r. (a -> Const rb) -> s -> Const rt . Aunque introdujimos nuevas variables de tipo y angustia mental para nosotros mismos, este tipo todavía es matemáticamente idéntico a lo que comenzamos con ( s -> a ).

Setter

Definir newtype Identity a = Identity a . Tenga en cuenta que la Identity a es la misma que a , matemáticamente y en tiempo de ejecución.
Ahora note que el type Setter stab = (a -> Identity b) -> s -> Identity t sigue siendo idéntico al tipo con el que comenzamos.

Todos juntos

Con este papeleo fuera del camino, ¿podemos unificar a los creadores y captadores en un solo tipo de Lens ?

type Setter s t a b = (a -> Identity b) -> s -> Identity t type Getter s t a b = forall r. (a -> Const r b) -> s -> Const r t

Bueno, esto es Haskell y podemos abstraer la elección de Identity o Const a una variable cuantificada. Como dice la lente wiki , todo lo que Const e Identity tienen en común es que cada uno es un Functor . Luego, elegimos eso como una especie de punto de unificación para estos tipos:

type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t

(También hay otras razones para elegir Functor , como probar las leyes de las referencias funcionales mediante el uso de teoremas libres. Pero aquí nos encargaremos un poco del tiempo). Eso para todos forall f es como el de todos. arriba: permite a los consumidores del tipo elegir cómo rellenar la variable. Rellene una Identity y obtendrá un configurador. Rellena una Const a y obtienes un getter. Fue mediante la elección de pequeñas y cuidadosas transformaciones en el camino que pudimos llegar a este punto.

Advertencias

Puede ser importante tener en cuenta que esta derivación no es la motivación original para el paquete de lens . Como lo explica la página de la wiki de Derivación , puede comenzar con el interesante comportamiento de (.) Con ciertas funciones y extraer la óptica desde allí. Pero creo que este camino que abrimos es un poco mejor para explicar la pregunta que planteaste, que era una pregunta importante que yo también estaba empezando. También quiero referirte a lentes sobre té , que proporciona otra derivación.

Creo que estas múltiples derivaciones son una buena cosa y una especie de varilla medidora para la salud del diseño de la lens . El hecho de que podamos llegar a la misma solución elegante desde diferentes ángulos significa que esta abstracción es robusta y está bien respaldada por diferentes intuiciones y matemáticas.

También mentí un poco sobre el tipo de Setter en lens recientes. Es en realidad

type Setter s t a b = forall f. Settable f => (a -> f b) -> s -> t b

Este es otro ejemplo de cómo abstraer el tipo de orden superior en tipos ópticos para brindar al usuario de la biblioteca una mejor experiencia. Casi siempre se creará una instancia de Identity , ya que hay una instance Settable Identity . Sin embargo, de vez en cuando es posible que desee pasar configuradores a la función backwards , que corrige f para ser la Backwards Identity . Probablemente podamos clasificar este párrafo como "más información acerca de la lens de la que probablemente querría saber".