idris - 如何创建一个只接受其他字段的字段？

Question

我想创建一个具有交替构造函数 Foo 和 Bar 的数据类型。例如，有效的成员是:

Foo (Bar (Foo (Bar End)))

但不是:

Foo (Foo (Bar End))

因为后者有两个连续的 Foo。在单个数据声明中表达这一点的正确方法是什么？

Answer 1

使用单个声明，您需要一个索引类型:

data Foo : Bool -> Type where
  End : Foo True
  Bar : Foo True -> Foo False
  Foo : Foo False -> Foo True

这与以下两种共同类型具有相同的居民:

data FooTrue = End | Foo FooFalse
data FooFalse = Bar FooTrue

一般来说，n 数据类型的共同族可以用由具有 n 元素的类型索引的单一类型族来表示。索引表示的优点是它允许通用操作，而这些操作对于相互类型来说是不可能的，因为可以对 {b : Bool} -> Foo b -> Foo b 或 等类型进行转换{b : Bool} -> Foo b -> Foo(不是 b)。像长度索引列表这样的无限共同族也只能通过索引类型实现。