在列表列表中,施加相同的长度

Question

我有这种数据类型,它应该代表一个表:

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

Answer 1

是的,有一种非常标准的方法来实现这一目标.但是,您支付的价格是您不能使用标准列表功能(因为您不会使用标准列表).这个想法是这样的:我们首先会有一个脊椎告诉所有"列表"有多长,然后我们将在脊柱的底部有实际的列表.您可以通过多种方式对列表的长度进行编码; 下面,我将展示如何使用简单的一元编号系统来完成它,但您当然可以使用其他编号系统设计更高效的版本.

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的" 制造数据类型"中将这种技术扩展到了一百个不同的方向.

Answer 2

你可以做到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,仅由自然数字的表示居住.

关键是,现在您还可以定义混合种类的类型构造函数.典型的例子是Vec:

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

这有点好Vec :: Nat -> * -> *.同样,T有种类T :: Nat -> *.这让你使用类型编码的常量长度,如果将两行不同的长度放在一起会导致类型错误.

虽然这看起来非常强大,但事实上它受到了限制.为了从这些表示中获取所有内容,依赖类型语言应该像Agda一样使用.