Hola Habr
El otro día, en uno de mis proyectos de hobby, surgió la tarea de escribir un repositorio de métricas.
La tarea en sí se resuelve de manera muy simple, pero mi problema con el Haskell (especialmente en proyectos para mi propio entretenimiento) es que es imposible simplemente tomar y resolver el problema. Es necesario decidir, expandir, abstraer, abstraer y luego expandir más. Por lo tanto, quería hacer extensible el almacenamiento de métricas para no especificar de antemano qué estarían allí. Esto en sí mismo es un tema para un artículo separado, y hoy consideraremos un pequeño ingrediente: escribir un contenedor seguro para tipos desconocidos anteriormente. Algo así como tipeo dinámico, pero con garantías estáticas de que no haremos tonterías.
Creo que el artículo no abrirá nada nuevo para los Haskellistas experimentados, pero ahora al menos sacaremos este ingrediente de la caja y no nos distraeremos en artículos posteriores. Bueno, o no puedes ser tan modesto y decir que ya se me ocurrió un patrón de diseño completo.
Entonces, primero formulamos el problema. Necesitamos poder asociar algunos objetos con valores de tipos previamente desconocidos. O, en otras palabras, es necesario que los valores de tipos previamente desconocidos actúen como claves en algún tipo de mapa.
Naturalmente, no estamos locos y no necesitaremos el apoyo de valores de ningún tipo. Requerimos que el tipo (incluso si se desconoce) admite la comparación en el sentido de ordenar. En términos de Haskell, esto significa que admitimos tipos a que implementan la clase Ord a .
Tenga en cuenta que podríamos exigir apoyo para tomar un hash y verificar la igualdad, pero por varias razones sería más conveniente y claro limitarnos a la comparación.
Cuando se trata de almacenar valores que se sabe que implementan algún tipo de clase, los tipos existenciales generalmente se usan en Haskell:
data SomeOrd where MkSomeOrd :: Ord a => a -> SomeOrd
Entonces, si se nos da un objeto de tipo SomeOrd y hacemos una coincidencia de patrón para él:
foo :: SomeOrd -> Bar foo (MkSomeOrd val) = ... (1) ...
entonces en el punto (1) no sabemos qué tipo tiene val , pero sabemos (y, lo más importante, el temporizador también sabe) que val implementa la clase de tiempo Ord .
Sin embargo, si las funciones de tipo de la clase implican dos (o más) argumentos, entonces el uso de dicho registro no es suficiente:
tryCompare :: SomeOrd -> SomeOrd -> Bool tryCompare (MkSomeOrd val1) (MkSomeOrd val2) = ?
Para usar los métodos Ord , es necesario que val y val2 mismo tipo, ¡pero esto no tiene que hacerse en absoluto! Resulta que nuestro SomeOrd inútil. Que hacer
A pesar de que Haskell es un lenguaje compilado con borrado de tipo agresivo (después de la compilación, generalmente están ausentes), el compilador aún puede generar representantes de tipo de tiempo de ejecución si se le pregunta al respecto. El rol representativo del tipo a es el valor del tipo TypeRep a , y solicitud la generación es respondida por la tipografía Typeable .
Por ciertoPor cierto, a no tiene que ser un tipo en el sentido habitual, es decir, pertenecer a una variedad * . Puede ser cualquier otro tipo de k , que teóricamente te permite hacer cosas geniales almacenando representantes de tiempo de ejecución de los tipos aprendidos y similares, pero aún no he descubierto exactamente qué.
Además, si tenemos dos instancias diferentes de rep1 :: TypeRep a, rep2 :: TypeRep b , podemos compararlas y verificar si representan el mismo tipo o no. Además, si en realidad representan el mismo tipo, entonces obviamente a coincide con b . Y, lo más importante, la función de verificar las representaciones de tipos para la igualdad devuelve un resultado que puede convencer al tipógrafo de esto:
eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2). TypeRep a -> TypeRep b -> Maybe (a :~~: b)
¿Qué tontería está escrita aquí?
Primero, eqTypeRep es una función.
En segundo lugar, es polimórfico, pero no solo por tipo, sino también por variedades de estos tipos. Esto se indica por la parte de forall k1 k2 (a :: k1) (b :: k2) ; esto significa que b no solo pueden ser tipos comunes como Int o [String] , sino también, por ejemplo, constructores notorios (ver DataKinds y otros intentos de certificar a Haskell). Pero no necesitamos todo esto.
En tercer lugar, acepta dos representaciones de tiempo de ejecución de tipos potencialmente diferentes, TypeRep a y TypeRep b .
Cuarto, devuelve un valor de tipo Maybe (a :~~: b) . Lo más interesante sucede aquí.
Si los tipos no coinciden, la función devuelve el Nothing habitual y todo está bien. Si los tipos coinciden, la función devuelve Just val , donde val es de tipo a :~~: b . Veamos de qué tipo es:
Ahora hablemos. Supongamos que obtenemos un valor val de tipo a :~~: b . ¿Cómo podría ser construido? La única forma es con el constructor HRefl , y este constructor requiere que en ambos lados del icono :~~: debería ser el mismo. Por lo tanto, a coincide con b . Además, si zapternnom-match en val , entonces el taypcheker también lo sabrá. Por lo tanto, sí, la función eqTypeRep devuelve la prueba de que dos tipos potencialmente diferentes son iguales si en realidad son iguales.
Sin embargo, en el párrafo anterior, mentí. Nadie nos impide escribir en Haskell algo así como
wrong :: Int :~~: String wrong = wrong
o
wrong :: Int :~~: String wrong = undefined
o romper el sistema con un montón de formas un poco menos obvias. Esta es una de las manifestaciones de lo conocido en círculos estrechos que dice que Haskell es inconsistente como lógica. En lenguajes con sistemas de tipos más fuertes, tales definiciones no están estampadas.
Es por eso que en la documentación mencionada anteriormente, se menciona el valor final . Ambas variantes de la implementación del wrong anterior no producen este valor final, lo que nos da un poco de razón y confianza: si nuestro programa en Haskell finalizó (y no se encontró con undefined ), entonces su resultado corresponde a los tipos escritos. Aquí, sin embargo, hay algunos detalles relacionados con la pereza, pero no abriremos este tema.
Y, por cierto, la segunda manifestación de la debilidad de Haskell en el código anterior es el tipo de la función eqTypeRep . En idiomas más fuertes, devolvería un valor de un tipo más fuerte, que no solo probaría la igualdad de los tipos si en realidad son iguales, sino que también demostraría su desigualdad si en realidad son desiguales. Sin embargo, la inconsistencia de la lógica de Haskell hace que tales funciones sean un poco inútiles: todo esto es importante cuando se usa el lenguaje como un probador de teoremas, y no como un lenguaje de programación, y no se usa a Haskell como un probador.
Bueno, suficiente de la teoría de registro y tipo, volvamos a nuestras métricas. Ahora solo dibuja un búho La discusión anterior insinúa que es suficiente almacenar en nuestro tipo existencial, esta también es la representación más en tiempo de ejecución del tipo, y todo estará bien.
Esto nos lleva a la siguiente implementación de nuestro tipo de contenedor:
data Dyn where Dyn :: Ord a => TypeRep a -> a -> Dyn toDyn :: (Typeable a, Ord a) => a -> Dyn toDyn val = Dyn (typeOf val) val
Ahora escribimos una función que toma lo siguiente:
- dos valores de tipo
Dyn ; - una función que produce algo para dos valores de cualquier tipo ,
basado solo en las constantes mencionadas al crear Dyn ( forall es responsable de esto),
y que se llama si ambos Dyn almacenan valores del mismo tipo; - y la función alternativa, que se llama en lugar de la anterior, si los tipos siguen siendo diferentes:
withDyns :: (forall a. Ord a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn -> Dyn -> b withDyns f def (Dyn ty1 v1) (Dyn ty2 v2) = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2
SomeTypeRep es un contenedor existencial sobre TypeRep a para cualquier a .
Ahora podemos implementar, por ejemplo, comprobación de igualdad y comparación:
instance Eq Dyn where (==) = withDyns (==) (\_ _ -> False) instance Ord Dyn where compare = withDyns compare compare
Aquí aprovechamos el hecho de que SomeTypeRep se puede comparar entre sí, por lo que también se compare la función de reserva para ordenar.
Listo
Solo que ahora es un pecado no generalizar: notamos que dentro de Dyn , toDyn , withDyns no usamos Ord específicamente, y esto podría ser cualquier otro conjunto de constantes, por lo que podemos habilitar la extensión ConstraintKinds y generalizar parametrizando Dyn conjunto específico de restricciones que nosotros necesario en nuestra tarea específica:
data Dyn ctx where Dyn :: ctx a => TypeRep a -> a -> Dyn ctx toDyn :: (Typeable a, ctx a) => a -> Dyn ctx toDyn val = Dyn (typeOf val) val withDyns :: (forall a. ctx a => a -> a -> b) -> (SomeTypeRep -> SomeTypeRep -> b) -> Dyn ctx -> Dyn ctx -> b withDyns (Dyn ty1 v1) (Dyn ty2 v2) f def = case eqTypeRep ty1 ty2 of Nothing -> def (SomeTypeRep ty1) (SomeTypeRep ty2) Just HRefl -> f v1 v2
Entonces Dyn Ord será nuestro tipo de Dyn Monoid y, por ejemplo, Dyn Monoid le permitirá almacenar monoides arbitrarios y hacer algo monoidal con ellos.
Escribamos las instancias que necesitamos para nuestro nuevo Dyn :
instance Eq (Dyn Eq) where (==) = withDyns (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns compare compare
... solo que esto no funciona. La máquina de escribir no sabe que Dyn Ord también implementa Eq ,
por lo tanto, debe copiar toda la jerarquía:
instance Eq (Dyn Eq) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Eq (Dyn Ord) where (==) = withDyns d1 d2 (==) (\_ _ -> False) instance Ord (Dyn Ord) where compare = withDyns d1 d2 compare compare
Bueno, ahora seguro.
... quizás, en un Haskell moderno, puede hacerlo para que el temporizador muestre instancias del formulario
instance C_i (Dyn (C_1, ... C_n)) where ...
porque sale algo prológico, pero aún no lo he hecho, tendré que sentarme a recogerlo. Estén atentos.
Y también, si Dyn ojos cuidadosamente, puedes ver que nuestro Dyn parece sospechosamente a un par dependiente del tipo (ty : Type ** val : ty) de los lenguajes crípticos. Pero solo en los idiomas que conozco es imposible hacer coincidir el tipo, porque la parametricidad (que en este caso, en mi humilde opinión, se interpreta demasiado), pero aquí parece posible.
Pero lo más importante: ahora puede tener de forma segura algo como Map (Dyn Ord) SomeValue y usar cualquier valor como clave, siempre que ellos mismos admitan la comparación. Por ejemplo, los identificadores con descripciones métricas se pueden usar como claves, pero este es un tema para el próximo artículo.