Могут ли системы хорошего типа различать матрицы в разных базах?

Ответ 1

Это очень хороший вопрос. Я не думаю, что вы можете кодировать понятие основы в большинстве систем типов, потому что, по существу, все, что делает контролер типов, должно быть в состоянии закончить, и суждения о том, являются ли два вещественных вектора равными, слишком сложны. Например, вы могли бы иметь (2 v_1) + (2 v_2) или 2 (v_1 + v_2). Существуют некоторые языки, которые используют зависимые типы [wikipedia], но они относительно академичны.

Я думаю, что большая часть вашей отладочной боли будет уменьшена, если вы просто закодируете основы, в которых ваша матрица работает вместе с матрицей. Например,

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

а затем, когда вы M от базиса a до b с N, проверьте, что N от b до c, и возвратите матрицу с основанием a в c.

ПРИМЕЧАНИЕ - кажется, большинство людей здесь имеют программирование вместо математического фона, поэтому я приведу здесь краткое объяснение. Матрицы - это кодировки линейных преобразований между векторными пространствами. Например, если вы кодируете поворот на 45 градусов в R ^ 2 (двухмерные реалы), тогда стандартный способ кодирования этого в матрице говорит, что стандартный базовый вектор e_1, написанный "[1, 0]", отправляется на комбинацию e_1 и e_2, а именно [1/sqrt (2), 1/sqrt (2)]. Дело в том, что вы можете кодировать одно и то же вращение, указывая, куда идут разные векторы, например, вы могли бы сказать, куда вы отправляете [1,1] и [1, -1] вместо e_1 = [1,0] и e_2 = [0,1], и это будет иметь другое представление матрицы.

Изменить 1

Если у вас есть конечный набор баз, с которыми вы работаете, вы можете это сделать...

{-# 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

Затем, в ghci (интерактивный интерпретатор 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

Ответ 2

Это вполне возможно в Haskell.

Статически проверенные размеры

Haskell имеет массивы с статически проверенными размерами, где размеры можно манипулировать и проверять статически, предотвращая индексирование в неправильный размер. Некоторые примеры:

Это будет работать на двухмерных массивах:

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

Пример из repa должен дать вам смысл. Здесь для получения диагонали требуется 2D-массив, возвращает 1D-массив того же типа.

diagonal :: Array DIM2 e -> Array DIM1 e

или из Matt sottile repa tutorial, статически проверенные размеры в трехмерном матричном преобразовании:

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'

Статически проверенные единицы

Другой пример из-за пределов матричного программирования: статически отмеченный единицы измерения, что делает его ошибкой типа, чтобы запутать например ногами и метрами, не делая преобразования.

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

или для целого набора единиц СИ и количествах.

например. не может добавлять вещи разного размера, такие как тома и длины:

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

Итак, следуя типам измерения размера repa -типа, я бы предложил добавить параметр типа Base phantom для ваш тип массива и использование этого для различения оснований. В Haskell индекс Dim аргумент типа дает ранг массива (т.е. его форму), и вы можете сделать аналогичным образом.

Или, если по базе вы подразумеваете некоторое измерение на единицах, используя типы размеров.

Итак, да, сейчас это почти товарная техника в Haskell, и есть некоторые примеры проектирования с такими типами, которые помогут вам начать работу.

Ответ 3

Хотя я понимаю, что это не строго касается (уточненного) вопроса - мои извинения - кажется актуальным, по крайней мере, по отношению к дону Стюарту популярный ответ...

Я являюсь автором библиотеки Haskell dimensional, на которую ссылался Дон и приводил примеры. Я также писал - несколько под радаром - экспериментальную рудиментарную библиотеку линейных алгебр основанную на размерности. Эта библиотека линейной алгебры статически отслеживает размеры векторов и матриц, а также физические размеры ( "единицы" ) их элементов на основе каждого элемента.

Эта последняя точка - отслеживание физических измерений на основе каждого элемента - является довольно сложной и, возможно, излишней для большинства применений, и можно даже утверждать, что она не имеет большого математического смысла иметь величины разных физических измерений в качестве элементов в любом заданном векторе/матрица. Однако некоторые интересующие меня приложения линейной алгебры, такие как фильтрация калмана и взвешенная оценка наименьших квадратов, обычно используют гетерогенные векторы состояний и ковариационные матрицы.

Используя фильтр Калмана в качестве примера, рассмотрим вектор состояния x = [d, v], который имеет физические размеры [L, LT ^ -1]. Следующий (будущий) вектор состояния предсказывается умножением на матрицу перехода состояния F, т.е. X '= F x_. Ясно, что для этого уравнения иметь смысл F не может быть произвольным, но должно иметь размер и физические размеры [[1, T], [T ^ -1, 1]]. Функция predict_x' ниже статически гарантирует, что это соотношение выполняется:

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

(неприглядный оператор |*< обозначает умножение матрицы слева с вектором справа.)

В общем случае для вектора состояния априорного x_ произвольного размера и с элементами произвольных физических измерений передача матрицы перехода состояния f с "несовместимым" размером и/или физическими размерами до predict_x' приведет к ошибка времени компиляции.

Ответ 4

В F # (который первоначально возник из OCaml) вы можете использовать единицы измерения. Эндрю Кеннед, который разработал эту функцию (а также создал очень интересную теорию), имеет большую статью, демонстрирующую ее.

Вполне вероятно, что это может быть использовано в вашем сценарии - хотя я не совсем понимаю этот вопрос. Например, вы можете объявить два типа блоков следующим образом:

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

Добавление литров и галлонов дает вам ошибку времени компиляции:

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

F # автоматически не вставляет преобразование между различными единицами, но вы можете написать функцию преобразования:

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

Прекрасная вещь об единицах измерения в F # заключается в том, что они автоматически выводятся и функции являются общими. Если вы умножаете 1.0<gallon> * 1.0<gallon>, результат равен 1.0<gallon^2>.

Люди использовали эту функцию для различных целей - от преобразования виртуальных счетчиков в пиксели экрана (в симуляции солнечной системы) до конвертации валют (в долларах в финансовых системах). Хотя я не эксперт, вполне вероятно, что вы можете каким-то образом использовать его для своего проблемного домена.

Ответ 5

Если он выражен в другой базе, вы можете просто добавить параметр шаблона в качестве базы. Это будет дифференцировать эти типы. A float - это float - это float - если вы не хотите, чтобы два значения float были одинаковыми, если они действительно имеют одинаковое значение, тогда вам нужно сообщить системе типов об этом.