Recursive definition of Matrix

Like Linked-list for Array, is there a recursive counter-part for Matrix?

Is there a persistent data structure which can be used in place of Matrix in pure functional language like Haskell?

• How about lists of lists? Since matrices are usually represented as arrays of arrays. – Anton Trunov Apr 25 '16 at 17:52
• I tries that. lists of lists works for decomposing matrix via row, but you can't decompose a matrix as head-column vector and tail matrix. when you decompose list as head and tail, you have tail list with original list. you can't decompose Matrix(list of lists) like that. – Satya Prakash Apr 25 '16 at 18:12
• What properties do you want the data structure to have? Usually we don't consider recursion as something valuable in itself; it's merely a means to an end, a way to achieve some other goal (like reducing memory consumption). – D.W. Apr 26 '16 at 6:38

Multiple Dimensions

For a recursive counterpart for matrices, we need dependent types.

Indeed, lists are one dimensional and so (horizontal) concatenation of lists is all that is needed. However, matrices are two dimensional and so concatenation may be meaningless if the sizes do not match up. That is to say, all rows need to have the same number of columns and likewise all columns need to have the same number of rows for a matrix to be (conventionally) meaningful. I mean, for example, usually no one thinks of, say, two rows that have two different length columns as being a matrix.

A Quick Implementation

So for concatenation, we need to keep track of the lengths. We can do so by using a language that supports dependent types, such as Idris or Agda. Haskell can mimic them, but a difficult task onto itself. So here's a naive implementation in Agda.

data Matrix (A : Set) : (rows columns : ℕ) → Set where
∣_∣ : A → Matrix A 1 1
_Φ_  : ∀ {r c₁ c₂} → Matrix A r c₁ → Matrix A r c₂ → Matrix A r (c₁ + c₂)
_⊝_  : ∀ {c r₁ r₂} → Matrix A r₁ c → Matrix A r₂ c → Matrix A (r₁ + r₂) c

The first constructor embeds the type A into 1-by-1 matrices and the other two constructors are for horizontal and vertical concatenation. Notice that the natural numbers are used to keep the matrices meaningful. For example, you can stick two matrices side-by-side to produce a wider matrix precisely if the two have the same number of rows.

For example, the 2-by-2 identity matrix

id₂ : Matrix ℕ 2 2
id₂ = (∣ 1 ∣ Φ ∣ 0 ∣) ⊝
(∣ 0 ∣ Φ ∣ 1 ∣)

Map

In one of the above comments, you remark that its troubling that we cannot pattern match and define recursive functions. Well, we can :-)

For example, the usual map of lists has a matrix counterpart.

map : ∀ {A B} (f : A → B) → ∀ {c r} → Matrix A r c → Matrix B r c
map f ∣ x ∣ = ∣ f x ∣
map f (m Φ m₁) = map f m Φ map f m₁
map f (m ⊝ m₁) = map f m ⊝ map f m₁

toString : ℕ → String
toString zero = "Zero"
toString (suc zero) = "One"
toString _ = "just no"

map-test : map toString id₂ ≡ (∣ "One"  ∣ Φ ∣ "Zero" ∣) ⊝
(∣ "Zero" ∣ Φ ∣ "One"  ∣)
map-test = refl

More Involved Example

As a more complicated example, let's consider matrices made by a single constant ---compare to Haskell's repeat operation that takes an element e and returns a list [e,e,...,e].

𝒦 : ∀ {A} → A → ∀{r c} → Matrix A (suc r) (suc c)
𝒦 e {0} {0} = ∣ e ∣                     -- 1x1 singleton matrix
𝒦 e {0} {c + 1} = ∣ e ∣ Φ 𝒦 e             -- row-vector of length r+1
𝒦 e {r + 1} {0} = ∣ e ∣ ⊝ 𝒦 e             -- column vector of length r+1
𝒦 e {r + 1} {c + 1} = (∣ e ∣ Φ 𝒦 e) ⊝ 𝒦 e -- (∣ e ∣ ⊝ 𝒦 e {m} {0}) Φ 𝒦 e {m+1}{c}

The last one says:

(    e  | 𝒦 e   )
𝒦 e {r+1} {c+1} =  (  ------------- )
( 𝒦 e {r} {c+1} )

Indeed any 𝒶×𝒷 matrix can be construed as the vertical concatenation of an 𝒶-row vector above an (𝒶-1)×𝒷 matrix ---note a recursion! In this case, our row vector is the element e followed by an r-row vector of e's.

Example usage:

test : 𝒦 5 {2} {2}
≡   (∣ 5 ∣ Φ ∣ 5 ∣ Φ ∣ 5 ∣) ⊝
(∣ 5 ∣ Φ ∣ 5 ∣ Φ ∣ 5 ∣) ⊝
(∣ 5 ∣ Φ ∣ 5 ∣ Φ ∣ 5 ∣)
test = refl

Sources

Of course, the implementation was brief and just to answer your question. A more full account can be found in the elegant lecture notes of Richard Bird.

Hope this helps!

• Nice. Perhaps it's worth noting that, with this approach, constructing a matrix gluing rows 00 and 11, and constructing another matrix gluing columns 01 and 01, lead to two distinct matrices even if they should be the same. I.e. the matrix "remembers" its construction recipe, so to speak. – chi Sep 27 '18 at 12:55
• Yes! As such, this is not a free construction since we need the horizontal-vertical constructions to be identified to obtain canonical forms. We could identify them by quotient but that is usually not provided in a language as it makes type checking undecidable. Still the above "inductive" approach is neat :-) Interestingly, we could try to re-type the constructors so that the rows must be formed before the columns and thereby obtain canonical forms... – Musa Al-hassy Sep 28 '18 at 15:35