haskell - unicoos - matriz asociada respecto a dos bases

¿Pueden los buenos sistemas tipográficos distinguir entre matrices en diferentes bases?

Question

Mi programa (Hartree-Fock / iterativo SCF) tiene dos matrices F y F ''que son realmente la misma matriz expresada en dos bases diferentes. Acabo de perder tres horas de tiempo de depuración porque accidentalmente usé F ''en lugar de F. En C ++, el comprobador de tipos no detecta este tipo de error porque ambas variables son objetos Eigen::Matrix<double, 2, 2> .

Me preguntaba, para el Haskell / ML / etc. personas, ya sea que estuvieras escribiendo este programa, habrías construido un sistema de tipos donde F y F ''tuvieran diferentes tipos? Como se veria eso? Básicamente estoy tratando de tener una idea de cómo puedo externalizar algunos errores lógicos en el comprobador de tipos.

Edición: La base de una matriz es como la unidad. Puedes decir 1L o por muchos galones, ambos significan lo mismo. O, para dar un ejemplo de vector, puede decir (0,1) en coordenadas cartesianas o (1, pi / 2) en polar. Pero aunque el significado es el mismo, los valores numéricos son diferentes.

Edit: Tal vez las unidades eran la analogía equivocada. No busco algún tipo de registro donde pueda especificar que el primer campo será litros y el segundo galón, sino una forma de decir que esta matriz como un todo, se define en términos de alguna otra matriz (la base), donde la base podría ser cualquier matriz de las mismas dimensiones. Por ejemplo, el constructor se parecería a mkMatrix [[1, 2], [3, 4]] [[5, 6], [7, 8]] y luego agregar ese objeto a otra matriz solo verificará el tipo si ambos Los objetos tenían la misma matriz que sus segundos parámetros. ¿Tiene sentido?

Edición: definición en Wikipedia , ejemplos trabajados

Answer 1

Aunque me doy cuenta de que esto no aborda estrictamente la pregunta (aclarada), mis disculpas, parece relevante al menos en relación con la popular respuesta de Don Stewart ...

Soy el autor de la biblioteca dimensional de Haskell a la que Don hizo referencia y proporcionó ejemplos de. También he estado escribiendo, algo bajo el radar, una biblioteca experimental de álgebra lineal rudimentaria basada en dimensiones . Esta biblioteca de álgebra lineal realiza un seguimiento estático de los tamaños de vectores y matrices, así como las dimensiones físicas ("unidades") de sus elementos por elemento.

Este último punto, el seguimiento de las dimensiones físicas por elemento, es bastante desafiante y quizás excesivo para la mayoría de los usos, y incluso se podría argumentar que tiene poco sentido matemático tener cantidades de diferentes dimensiones físicas como elementos en cualquier vector / matriz dada. Sin embargo, algunas aplicaciones de álgebra lineal que me interesan, como el filtrado de kalman y la estimación de mínimos cuadrados ponderados, suelen utilizar vectores de estado heterogéneos y matrices de covarianza.

Usando un filtro de Kalman como ejemplo, considere un vector de estado x = [d, v] que tiene dimensiones físicas [L, LT ^ -1] . El siguiente vector de estado (futuro) se predice mediante la multiplicación por la matriz de transición de estado F , es decir: x ''= F x_ . Claramente, para que esta ecuación tenga sentido, F no puede ser arbitraria, pero debe tener tamaño y dimensiones físicas [[1, T], [T ^ -1, 1]] . La predict_x'' función de predict_x'' asegura estáticamente que esta relación se mantiene:

predict_x'' :: (Num a, MatrixVector f x x) => Mat f a -> Vec x a -> Vec x a
predict_x'' f x_ = f |*< x_

(El operador antiestético |*< denota la multiplicación de una matriz a la izquierda con un vector a la derecha).

Más generalmente, para un vector de estado a priori x_ de tamaño arbitrario y con elementos de dimensiones físicas arbitrarias, pasar una matriz de transición de estado f con tamaño "incompatible" y / o dimensiones físicas para predict_x'' causará un error de tiempo de compilación.

Answer 2

En F # (que originalmente evolucionó desde OCaml), puede usar unidades de medida . Andrew Kenned, quien diseñó la característica (y también creó una teoría muy interesante detrás de ella) tiene una gran serie de artículos que lo demuestran .

Es muy probable que esto se pueda usar en su escenario, aunque no entiendo completamente la pregunta. Por ejemplo, puedes declarar dos tipos de unidades como esta:

[<Measure>] type litre
[<Measure>] type gallon

Agregar litros y galones le da un error de tiempo de compilación:

1.0<litre> + 1.0<gallon> // Error!

F # no inserta automáticamente la conversión entre diferentes unidades, pero puede escribir una función de conversión:

let toLitres gal = gal * 3.78541178<litre/gallon>
1.0<litre> + (toLitres 1.0<gallon>)

Lo bello de las unidades de medida en F # es que se deducen automáticamente y las funciones son genéricas. Si multiplicas 1.0<gallon> * 1.0<gallon> , el resultado es 1.0<gallon^2> .

La gente ha utilizado esta función para varias cosas, desde la conversión de medidores virtuales a píxeles de pantalla (en simulaciones del sistema solar) hasta la conversión de monedas (dólares en sistemas financieros). Aunque no soy un experto, es muy probable que también pueda usarlo de alguna manera para su dominio de problema.

Answer 3

Esta es una muy buena pregunta. No creo que pueda codificar la noción de una base en la mayoría de los sistemas de tipo, porque esencialmente cualquier cosa que haga el verificador de tipos debe poder terminar, y es difícil determinar si dos vectores de valor real son iguales. Podría tener (2 v_1) + (2 v_2) o 2 (v_1 + v_2), por ejemplo. Hay algunos idiomas que usan tipos dependientes [ wikipedia ], pero estos son relativamente académicos.

Creo que la mayor parte de su dolor de depuración se aliviaría si simplemente codificara las bases en las que trabaja la matriz junto con la matriz. Por ejemplo,

newtype Matrix = Matrix { transform :: [[Double]],
srcbasis :: [Double], dstbasis :: [Double] }

y luego, cuando M desde la base a hasta b con N , verifique que N sea ​​de b a c , y devuelva una matriz con la base a a c .

NOTA : parece que la mayoría de las personas aquí tienen antecedentes de programación en lugar de matemáticos, por lo que proporcionaré una breve explicación aquí. Las matrices son codificaciones de transformaciones lineales entre espacios vectoriales. Por ejemplo, si está codificando una rotación de 45 grados en R ^ 2 (reales bidimensionales), entonces la forma estándar de codificar esto en una matriz es decir que el vector de base estándar e_1, escrito "[1, 0] ", se envía a una combinación de e_1 y e_2, a saber, [1 / sqrt (2), 1 / sqrt (2)]. El punto es que puede codificar la misma rotación diciendo dónde van los diferentes vectores, por ejemplo, podría decir dónde está enviando [1,1] y [1, -1] en lugar de e_1 = [1,0] y e_2 = [0,1], y esto tendría una representación de matriz diferente.

Editar 1

Si tienes un conjunto finito de bases con las que estás trabajando, puedes hacerlo ...

{-# LANGUAGE EmptyDataDecls #-}
data BasisA
data BasisB
data BasisC
newtype Matrix a b = Matrix { coefficients :: [[Double]] }
multiply :: Matrix a b -> Matrix b c -> Matrix a c
multiply (Matrix a_coeff) (Matrix b_coeff) = (Matrix multiplied) :: Matrix a c
where multiplied = undefined -- your algorithm here

Luego, en ghci (el intérprete interactivo de Haskell),

*Matrix> let m = Matrix [[1, 2], [3, 4]] :: Matrix BasisA BasisB
*Matrix> m `multiply` m
<interactive>:1:13:
Couldn''t match expected type `BasisB''
against inferred type `BasisA''
*Matrix> let m2 = Matrix [[1, 2], [3, 4]] :: Matrix BasisB BasisC
*Matrix> m `multiply` m2
-- works after you finish defining show and the multiplication algorithm

Answer 4

Esto es completamente posible en Haskell.

Dimensiones revisadas estáticamente

Haskell tiene matrices con dimensiones comprobadas estáticamente , donde las dimensiones pueden manipularse y comprobarse estáticamente, evitando la indexación en la dimensión incorrecta. Algunos ejemplos:

Esto solo funcionará en arreglos 2-D :

multiplyMM :: Array DIM2 Double -> Array DIM2 Double -> Array DIM2 Double

Un ejemplo de repa debería darte un sentido. Aquí, tomar una diagonal requiere una matriz 2D, devuelve una matriz 1D del mismo tipo.

diagonal :: Array DIM2 e -> Array DIM1 e

o, del tutorial de repa de Matt sottile , verificó estáticamente las dimensiones en una transformación de matriz 3D:

f :: Array DIM3 Double -> Array DIM2 Double
f u =
let slabX = (Z:.All:.All:.(0::Int))
slabY = (Z:.All:.All:.(1::Int))
u'' = (slice u slabX) * (slice u slabX) +
(slice u slabY) * (slice u slabY)
in
R.map sqrt u''

Unidades comprobadas estáticamente

Otro ejemplo desde fuera de la programación matricial: unidades de dimensión controladas estáticamente, lo que hace que sea un error de tipo confundir, por ejemplo, pies y metros, sin hacer la conversión.

 Prelude> 3 *~ foot + 1 *~ metre
1.9144 m

o para un conjunto completo de unidades y unidades SI .

Por ejemplo, no se pueden agregar elementos de diferentes dimensiones, como volúmenes y longitudes:

> 1 *~ centi litre + 2 *~ inch
Error:
Expected type: Unit DVolume a1
Actual type: Unit DLength a0

Por lo tanto, siguiendo los tipos de dimensión de matriz de estilo repa , sugeriría agregar un parámetro de tipo fantasma Base a su tipo de matriz y usarlo para distinguir entre las bases. En Haskell, el argumento de tipo Dim del índice da el rango de la matriz (es decir, su forma), y usted podría hacer lo mismo.

O, si por base te refieres a alguna dimensión en las unidades, usando tipos dimensionales.

Entonces, sí, esta es casi una técnica básica en Haskell ahora, y hay algunos ejemplos de diseño con tipos como este para ayudarlo a comenzar.

Answer 5

Si se expresa en una base diferente, simplemente puede agregar un parámetro de plantilla para que actúe como la base. Eso diferenciará esos tipos. Un float es un float es un float : si no desea que dos valores float sean iguales si en realidad tienen el mismo valor, debe informar al sistema de tipos al respecto.