我有这个数据类型，应该代表一个表格：
data R = R [Bool] deriving Eq -- Row
data T = T [R] deriving Eq -- Table
问题是它允许有不同长度的行表，例如：
tab =T [R [True, False, True, True],
R [False, False, True, False],
R [False, False, False, True],
R [False, False]]
是否可以修改T 的数据定义以强制所有R 元素具有相同的长度？
【问题讨论】：
标签： haskell
是的，有一种非常标准的方法可以实现这一目标。但是，您付出的代价是您无法使用标准列表功能（因为您不会使用标准列表）。这个想法是这样的：我们首先有一个脊椎告诉所有“列表”有多长，然后我们将在脊椎底部有实际的列表。您可以通过多种方式对列表的长度进行编码；下面，我将只展示如何使用简单的一元编号系统来实现，但您当然可以使用其他编号系统设计更高效的版本。
data BalancedLists_ a as
= Nil [as]
| Cons (BalancedLists_ a (a, as))
type BalancedLists a = BalancedLists_ a ()
例如，包含两个长度为 3 的列表的平衡列表如下所示：
Cons (Cons (Cons (Nil [(1, (2, (3, ()))), (4, (5, (6, ())))])))
Ralf Hinze 有一篇很棒的论文将这项技术扩展到一百个不同的方向，称为Manufacturing Datatypes。
【讨论】：
您可以使用DataKinds 做到这一点。不过，这可能过于复杂：
{-# LANGUAGE DataKinds, KindSignatures, GADTs #-}
-- requires 7.4.1, I think
data Nat = S Nat | Z
infixr 0 :.
data R (n :: Nat) where
Nil :: R Z -- like []
(:.) :: Bool -> R n -> R (S n) -- and (:)
data T (n :: Nat) = T [R n]
-- OK
test1 = T [(True :. True :. Nil), (True :. False :. Nil)]
-- will fail
test2 = T [(True :. True :. Nil), (False :. Nil)]
我宁愿推荐@MathematicalOrchids 使用智能构造函数的替代方法。
编辑：DataKinds 做什么。
DataKinds 扩展允许编译器为每个写入的数据类型自动创建一个新类型，而不是 *，以及来自构造函数的这种类型的新类型。
所以Nat，除了是一个简单的ADT，还产生了一种Nat，以及类型构造函数Z :: Nat和S :: Nat -> Nat。这个S 与Maybe :: * -> * 相当——它只是不使用所有类型的类型，而是你的新类型Nat，只包含自然数的表示。
重点是，现在您还可以定义 mixed 种类的类型构造函数。这方面的经典例子是Vec：
data Vec (n :: Nat) (a :: *) where {-...-}
有一种Vec :: Nat -> * -> *。类似地，T 具有类型 T :: Nat -> *。这让您可以将它与类型编码的常量长度一起使用，如果将两行不同长度的行放在一起，则会导致类型错误。
虽然这看起来非常强大，但实际上是受到限制的。要从这种表示中获取所有内容，应该使用依赖类型的语言，例如 Agda。
【讨论】：
Nat 是内置的，您可以在类型级别使用数字文字。
list 类型表示任意大小的容器。您可以使用 tuple 来强制执行特定大小 - 但它仅适用于“小”大小。例如：
data R = R (Bool, Bool, Bool, Bool) deriving Eq
现在每行总是正好包含 4 个单元格。
如果您真正想要的是强制行可以是 any 大小，只要它与表中的所有行的 相同...要困难得多。有几种方法可以在类型系统中对此进行编码，但没有一种是特别“简单”的。
另一种选择是在运行时强制执行条件，而不是尝试在编译时保证它。您可以编写一个定义行和表类型的模块，但隐藏它们的定义，并且只公开用于处理这些类型的函数，这些函数保留您想要的不变性（即所有行的长度相等）。
【讨论】：
There are several ways to encode this in the type system, but none of them are especially "simple". - 我对了解其中一种方法非常感兴趣。 :-)
还有一种方法是使用Data.Array。它的一个好处是它允许真正的多维数组，而不是数组的数组。只需使用元组来索引Array。
【讨论】：
Data.Array限制所有行的长度？
(1, 1) 到 (6, 10)，则数组有 6 行和 10 列。该范围内的每个索引都存在并具有相应的数组元素。行（或列）不可能大小不等。