Linear Algebra in Idris 2: Dependent Types with Matrices

In Idris 2, vectors and matrices can encode their dimensions directly in their types. This allows the type checker to statically guarantee that operations like addition and multiplication are only performed on matrices with compatible dimensions.

1. Defining Vectors and Matrices

We represent a vector of a specific length using Vect n a. A matrix with m rows and n columns is defined as a vector of length m, where each element is a vector of length n.

module MatrixOps

import Data.Vect

||| A Matrix with `m` rows and `n` columns containing elements of type `a`.
public export
Matrix : Nat -> Nat -> Type -> Type
Matrix m n a = Vect m (Vect n a)

2. Matrix Addition

Matrix addition requires two matrices to have the exact same dimensions ($m \times n$). We can define this concisely using zip-wise operations (zipWith).

||| Adds two m x n matrices element-wise.
public export
addMatrix : Num a => Matrix m n a -> Matrix m n a -> Matrix m n a
addMatrix = zipWith (zipWith (+))

Explanation:

• The inner zipWith (+) adds two 1D vectors of length n element-wise.
• The outer zipWith applies this vector-addition operation across all m rows.

3. Matrix Transpose

Transposing an $m \times n$ matrix results in an $n \times m$ matrix. In Idris, this is remarkably simple thanks to transpose provided in Data.Vect.

||| Transposes an m x n matrix into an n x m matrix.
public export
transposeMatrix : Matrix m n a -> Matrix n m a
transposeMatrix = transpose

Explanation:

• Idris's standard library Data.Vect.transpose leverages sequence over vectors, cleanly swapping the row and column dimensions at the type level.

4. Matrix Multiplication

Matrix multiplication multiplies an $m \times k$ matrix by a $k \times n$ matrix to yield an $m \times n$ matrix.

We can define a helper for the dot product of two vectors, then combine it with matrix transposition.

||| Computes the dot product of two vectors of equal length.
public export
dotProduct : Num a => Vect k a -> Vect k a -> a
dotProduct v1 v2 = sum (zipWith (*) v1 v2)

||| Multiplies an (m x k) matrix by a (k x n) matrix to get an (m x n) matrix.
public export
multMatrix : Num a => Matrix m k a -> Matrix k n a -> Matrix m n a
multMatrix mat1 mat2 =
  let mat2T = transposeMatrix mat2
   in map (\row => map (dotProduct row) mat2T) mat1

Explanation:

1. transposeMatrix mat2: Transposes the right matrix from $k \times n$ to $n \times k$. This allows us to easily compute dot products between rows of mat1 and columns of mat2 (which are now rows in mat2T).
2. map (\row => ...): Iterates over each row in mat1.
3. map (dotProduct row) mat2T: Computes the dot product of the current row of mat1 with every row (column) of mat2T.

5. Complete Runnable Code & Example

Below is a complete, self-contained module demonstrating the operations in action.

module Main

import Data.Vect

Matrix : Nat -> Nat -> Type -> Type
Matrix m n a = Vect m (Vect n a)

addMatrix : Num a => Matrix m n a -> Matrix m n a -> Matrix m n a
addMatrix = zipWith (zipWith (+))

transposeMatrix : Matrix m n a -> Matrix n m a
transposeMatrix = transpose

dotProduct : Num a => Vect k a -> Vect k a -> a
dotProduct v1 v2 = sum (zipWith (*) v1 v2)

multMatrix : Num a => Matrix m k a -> Matrix k n a -> Matrix m n a
multMatrix mat1 mat2 =
  let mat2T = transposeMatrix mat2
   in map (\row => map (dotProduct row) mat2T) mat1

-- Example Matrices
mA : Matrix 2 3 Int
mA = [ [1, 2, 3]
     , [4, 5, 6]
     ]

mB : Matrix 3 2 Int
mB = [ [7, 8]
     , [9, 10]
     , [11, 12]
     ]

mC : Matrix 2 3 Int
mC = [ [1, 1, 1]
     , [2, 2, 2]
     ]

main : IO ()
main = do
  putStrLn "--- Matrix Addition (mA + mC) ---"
  printLn (addMatrix mA mC)

  putStrLn "\n--- Transpose (transpose mA) ---"
  printLn (transposeMatrix mA)

  putStrLn "\n--- Matrix Multiplication (mA * mB) ---"
  printLn (multMatrix mA mB)