方形矩阵的嵌套数据类型 [英] Nested datatype for square matrices

问题描述

我试图了解这种数据类型(方)如何表示平方矩阵.

I am trying to understand how this datatype (Square) represents square matrices.

type Square = Square' Nil
data Square' t a = Zero (t (t a) ) | Succ (Square' (Cons t) a)
data Nil a = Nil
data Cons t a = Cons a (t a)

所以. t在这里是什么?我想这是上面声明的类型之一. 我决定从最简单的开始，所以

So. What is t here? I suppose it is one of the types declared above. I decided to start with the simplest, so

Zero (Nil (Nil Int))

如果我将整数4作为值，这是矩阵(4)吗?

If I put integer 4 as a value, is this a matrix (4)?

假设它是某种东西.现在，这是什么:

Suppose it is something. Now, what is this:

Succ ( Zero (Cons t) a) 

如果我对t说的没错，那么也许这必须代表一些2×2矩阵，但是它的值是多少?

if I am right about t, then this, perhaps, must represent some 2×2 matrix, but what are its values?

Succ (Zero (Cons Nil) a) 

感谢您对我的方形矩阵理解的帮助.

I would appreciate your help in my understanding of how it is a square matrix.

推荐答案

让我们介绍一些非正式的符号来指导直觉.写T :> U表示T是具有一个或多个子情况的和类型，而U是其中一个子情况(至少对某些同构取模).我们还将在类型之间使用=表示同构.

Let's introduce some informal notation to guide intuition. Write T :> U to denote that T is a sum type having one or more subcases, and U is one of them (at least modulo some isomorphism). We'll also use = between types to denote isomorphism.

因此，根据定义，我们有

So, by definition, we have

Square a = Square' Nil a
:> { taking the Zero branch }
Nil (Nil a)
=
()

因此，这种情况表示空的"0x0"矩阵.

So, this case denotes the empty "0x0" matrix.

Square a = Square' Nil a
:> { taking the Succ branch }
Square' (Cons Nil) a
:> { taking the Zero branch }
Cons Nil (Cons Nil a)
=  { def of Cons }
(Cons Nil a, Nil (Cons Nil a))
=  { def of Cons }
((a, Nil a), Nil (Cons Nil a))
=  { def of Nil }
((a, ()), ())
=
a

所以，这是1x1矩阵.

So, this is the 1x1 matrix.

Square a = Square' Nil a
:> { taking the Succ branch }
Square' (Cons Nil) a
:> { taking the Succ branch again }
Square' (Cons (Cons Nil)) a
:> { taking the Zero branch }
Cons (Cons Nil) (Cons (Cons Nil) a)
=
Cons (Cons Nil) (a, Cons Nil a)
=
Cons (Cons Nil) (a, a, Nil a)
=
Cons (Cons Nil) (a, a, ())
=
Cons (Cons Nil) (a, a)
=
((a,a), Cons Nil (a, a))
=
((a,a), (a,a), Nil (a, a))
=
((a,a), (a,a), ())
=
((a,a), (a,a))

所以，这是2x2矩阵.

So, this is the 2x2 matrix.

我们现在应该能够发现一些模式.以Succ分支，我们最终得到一种形式的

We should now be able to spot some pattern. Taking the Succ branches, we end up with a type of the form

Square' (Cons (Cons (Cons (...(Cons Nil))))) a

最后一个Zero变为

F (F a)
  where F = (Cons (Cons (Cons (...(Cons Nil)))))

请注意，我们考虑了所有可能的情况，因此最终类型确实必须为F (F a)形式，而某些F则为上述形式.

Note that we considered all possible cases, so the final type must indeed be of the form F (F a) with some F of the form above.

现在，可以看到F a与(a,a,a,....)同构，其中a的数字N恰好是F定义中的Cons es的数字N.因此，F (F a)将产生一个方矩阵(N元组的N元组=方矩阵).

Now, one can see that F a is isomorphic to (a,a,a,....) where the number N of as it exactly the number N of Conses in the definition of F. Hence, F (F a) will produce a square matrix (an N-tuple of N-tuples = square matrix).

让我们通过归纳Cons es的数量来证明这一点.对于零的情况，我们有F = Nil，实际上，正如我们想要的，零a出现了:

Let's prove that by induction on the number of Conses. For the zero case, we have F = Nil, and indeed, as we wanted, zero as appear:

Nil a = ()

对于归纳情况，假定具有N Cons es的F a是具有N a s的(a,a,...).要证明的N + 1情况将说明(Cons F) a是(a,a,...,a)，具有N + 1 a s个.确实:

For the induction case, assume F a with N Conses is (a,a,...) with N as. The N+1 case to prove would state that (Cons F) a is (a,a,...,a), having N+1 as. Indeed:

Cons F a
=
(a, F a)
=
(a, (a,a....))   { 1 + N a's , as wanted }

QED.

这篇关于方形矩阵的嵌套数据类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！