平方矩阵的嵌套数据类型

Question

我试图了解此数据类型（方）如何表示平方矩阵。

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什么 我想这是上面声明的类型之一。我决定从最简单的开始

Zero (Nil (Nil Int))

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

假设它是某种东西。现在，这是什么：

Succ ( Zero (Cons t) a) 

如果我是正确的t，那么这也许必须代表一些2×2矩阵，但是它的值是多少？

Succ (Zero (Cons Nil) a) 

感谢您在我对它是方矩阵的理解方面的帮助。

Answer 1

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

因此，根据定义，我们有

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

因此，这种情况表示空的“ 0x0”矩阵。

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矩阵。

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矩阵。

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

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

最终Zero，

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

请注意，我们考虑了所有可能的情况，因此最终类型的确必须F (F a)具有F上面某些形式的形式。

现在，人们可以看到，F a同构(a,a,a,....)，其中数N a的IT确切的数N Cons的定义中，ES F。因此，F (F a)将产生一个方矩阵（N个元组的N个元组=方矩阵）。

让我们通过归纳Conses 数来证明这一点。对于零的情况，我们有F = Nil，实际上，正如我们想要的，零a出现：

Nil a = ()

对于感应情况，假设F aN Conses为(a,a,...)N as。要证明的N + 1种情况将陈述(Cons F) a为(a,a,...,a)N + 1个a。确实：

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

QED。