Recursive Matrix definition

Matrix.fm

// Standard construction of Matrix based on Vector
//T Matrix <A: Type> ~ (rows: Nat, cols: Nat)
//| matrix<rows:Nat,cols:Nat>(vecs: Vector(Vector(A,cols),rows)) ~ (rows,cols);

Matrix(A: Type, n: Nat, m: Nat) : Type
  matrix<P: (n: Nat) -> (m: Nat) -> Matrix(A,n,m) -> Type> ->
  (znil: P(Nat.0,Nat.0,Matrix.znil<A>)) ->
  (rnil: P(Nat.1,Nat.0, Matrix.rnil<A>)) ->
  (cnil: P(Nat.0,Nat.1, Matrix.cnil<A>)) ->
  (cell: (x : A) -> P(Nat.1,Nat.1, Matrix.cell<A>(x))) ->
  (cols: <n: Nat> -> <a: Nat> -> <b: Nat> ->
         (x: Matrix(A,n,a)) -> (y: Matrix(A,n,b)) ->
         P(n,Nat.add(a,b),Matrix.cols<A,n,a,b>(x,y))) ->
  (rows: <m: Nat> -> <a: Nat> -> <b: Nat> ->
         (x: Matrix(A,a,m)) -> (y: Matrix(A,b,m)) ->
         P(Nat.add(a,b),m,Matrix.rows<A,m,a,b>(x,y))) ->
  P(n,m,matrix)

// the 0x0 empty matrix
Matrix.znil<A: Type> : Matrix(A,Nat.0,Nat.0)
  <P> (znil) (rnil) (cnil) (cell) (cols) (rows) znil

// an empty row, needed because all n x 0 matrices are also empty, but not constructible from znil alone
Matrix.rnil<A: Type> : Matrix(A,Nat.1,Nat.0)
  <P> (znil) (rnil) (cnil) (cell) (cols) (rows) rnil

// empty column
Matrix.cnil<A: Type> : Matrix(A,Nat.0,Nat.1)
  <P> (znil) (rnil) (cnil) (cell) (cols) (rows) cnil

// promote value to a 1x1 matrix
Matrix.cell<A: Type>(x: A): Matrix(A,Nat.1,Nat.1)
  <P> (znil) (rnil) (cnil) 
  (cell) (cols) (rows) cell(x)

// join matrices by columns
Matrix.cols<A: Type, n: Nat, a: Nat, b: Nat>(x: Matrix(A,n,a), y: Matrix(A,n,b))
  : Matrix(A,n,Nat.add(a,b))
  <P> (znil) (rnil) (cnil) 
  (cell) (cols) (rows) cols<n,a,b>(x,y)

// join matrices by rows
Matrix.rows<A: Type, m: Nat, a: Nat, b: Nat>(x: Matrix(A,a,m), y: Matrix(A,b,m))
  : Matrix(A,Nat.add(a,b),m)
  <P> (znil) (rnil) (cnil) 
  (cell) (cols) (rows) rows<m,a,b>(x,y)

// notation convention:
// , = cols, + = rows, | | = cell

// |1,2|
Matrix.test1: Matrix(Nat,Nat.1,Nat.2)
  Matrix.cols<Nat,Nat.1,Nat.1,Nat.1>(Matrix.cell<Nat>(Nat.1), Matrix.cell<Nat>(Nat.2))

// |3,4|
Matrix.test2: Matrix(Nat,Nat.1,Nat.2)
  Matrix.cols<Nat,Nat.1,Nat.1,Nat.1>(Matrix.cell<Nat>(Nat.3), Matrix.cell<Nat>(Nat.4))

// |1| + |3|
Matrix.test3: Matrix(Nat,Nat.2,Nat.1)
  Matrix.rows<Nat,Nat.1,Nat.1,Nat.1>(Matrix.cell<Nat>(Nat.1), Matrix.cell<Nat>(Nat.3))

// |2| + |4|
Matrix.test4: Matrix(Nat,Nat.2,Nat.1)
  Matrix.rows<Nat,Nat.1,Nat.1,Nat.1>(Matrix.cell<Nat>(Nat.2), Matrix.cell<Nat>(Nat.4))

// | 1 2 |
// | 3 4 | =  |1| + |3|, |2| + |4|
Matrix.test5: Matrix(Nat,Nat.2,Nat.2)
  Matrix.cols<Nat,Nat.2,Nat.1,Nat.1>(Matrix.test3,Matrix.test4)

// | 1 2 |
// | 3 4 | = |1,2| + |3,4|
Matrix.test6: Matrix(Nat,Nat.2,Nat.2)
  Matrix.rows<Nat,Nat.2,Nat.1,Nat.1>(Matrix.test1,Matrix.test2)

// Unfortunately the order of joins matters, since we don't reduce matrices to canonical forms.
// Next step could be using smart constructors.
//Matrix.eq1: Equal(Matrix(Nat,Nat.2,Nat.2),Matrix.test5,Matrix.test6)
//  Equal.to<Matrix(Nat,Nat.2,Nat.2),Matrix.test5>