4

我有这个数据类型，它应该代表一个表：

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元素具有相同的长度？

4

4 回答 4

10

是的，有一种非常标准的方法可以实现这一目标。然而，您付出的代价是您无法使用标准列表函数（因为您不会使用标准列表）。这个想法是这样的：我们首先有一个脊椎告诉所有“列表”有多长，然后我们将在脊椎底部有实际的列表。您可以通过多种方式对列表的长度进行编码；下面，我将只展示如何使用简单的一元编号系统来实现，但您当然可以使用其他编号系统设计更高效的版本。

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有一篇精彩的论文将这项技术扩展到一百个不同的方向，称为制造数据类型。

于 2012-09-19T13:16:12.217 回答
8

你可以用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 之外，还产生了 kindNat和 type 构造函数Z :: Nat和S :: Nat -> Nat. 这S与Maybe :: * -> *- 它只是不使用所有类型的 kind ，而是您的新 kind Nat，仅由自然数的表示形式存在。

关键是，现在您还可以定义混合类型的类型构造函数。典型的例子是Vec：

data Vec (n :: Nat) (a :: *) where {-...-}

有种Vec :: Nat -> * -> *。同样，T有 kind T :: Nat -> *。这让您可以将其与类型编码的常量长度一起使用，如果将两行不同长度的行放在一起，则会导致类型错误。

虽然这看起来非常强大，但实际上是受到限制的。为了从这种表示中得到所有东西，应该使用像Agda这样的依赖类型语言。

于 2012-09-19T10:41:46.377 回答
4

列表类型表示任意大小的容器。您可以使用元组来强制执行特定大小 - 但它仅对“小”大小才真正可行。例如：

data R = R (Bool, Bool, Bool, Bool) deriving Eq

现在每一行总是正好包含 4 个单元格。

如果您真正想要的是强制行可以是任何大小，只要它对于表中的所有行都相同......那就更困难了。有几种方法可以在类型系统中对此进行编码，但没有一种方法特别“简单”。

另一种选择是在运行时强制执行条件，而不是试图在编译时保证它。您可以编写一个定义行和表类型的模块，但隐藏它们的定义，并且只公开用于处理这些类型的函数，这些函数保留了您想要的不变量（即，所有行的长度相等）。

于 2012-09-19T09:58:49.143 回答
1

还有一种方法是使用Data.Array. 它的一个好处是它允许真正的多维数组，而不是数组的数组。只需使用元组来索引Array.

于 2012-09-19T22:47:14.547 回答