¿Pueden los buenos sistemas de tipos distinguir entre matrices en diferentes bases?

Esto es completamente posible en Haskell.

Dimensiones verificadas estáticamente

Haskell tiene matrices con dimensiones verificadas estáticamente, donde las dimensiones se pueden manipular y comprobar estáticamente, evitando la indexación en la dimensión incorrecta. Algunos ejemplos:

Esto solo funcionará en matrices 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 1D matriz del mismo tipo.

diagonal :: Array DIM2 e -> Array DIM1 e

O, de El tutorial repa de Matt sottile , dimensiones verificadas estáticamente en una transformada 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 estáticamente verificadas

Otro ejemplo fuera de la programación matricial: estáticamente comprobado unidades de dimensión, por lo que es un error de tipo para 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 cuantificaciones del SI.

Por ejemplo, no se pueden agregar cosas de diferente dimensión, 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 bases. En Haskell, el índice Dim type argumento 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 dimensional tipo.

Así que, sí, esto es casi una técnica de productos básicos en Haskell ahora, y hay algunos ejemplos de diseño con tipos como este para ayudarle a empezar.

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

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

Este último punto – el seguimiento de las dimensiones físicas sobre una base por elemento – es bastante desafiante y quizás excesivo para la mayoría de los usos, e incluso se podría argumentar que tiene poco sentido matemático tener cantidades de diferentes dimensiones físicas como elementos en cualquier vector/matriz dado. Sin embargo, algunas aplicaciones de álgebra lineal de interés para mí, tales como kalman filtrado y ponderado la estimación de mínimos cuadrados generalmente utiliza 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) es predicho por 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 sino que debe tener tamaño y dimensiones físicas [[1, T], [T^-1, 1]]. La función predict_x' debajo estáticamente asegura que esta relación se mantenga:

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

(El antiestético operador |*< 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 a predict_x' causará un tiempo de compilación error.

En F# (que originalmente evolucionó de OCaml), puedes usar unidades de medida. Andrew Kenned, quien diseñó la función (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 use en su escenario, aunque no entiendo completamente la pregunta. Por ejemplo, puede declarar dos tipos de unidad como este:

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

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

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 bueno de las unidades de medida en F# es que se deducen automáticamente y las funciones son genéricas. Si multiplica 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 pueda usarlo de alguna manera para su dominio del problema también.

Si se expresa en una base diferente, simplemente puede agregar un parámetro de plantilla para que actúe como base. Eso diferenciará esos tipos. A float es a float es a float - si no desea que dos valores float sean los mismos si realmente tienen el mismo valor, entonces debe informar al sistema de tipos al respecto.