haskell - 数据的所有约束都可以表示为代数数据类型吗？

Question

数据和状态的所有约束都可以表示为代数数据类型吗？

我喜欢这种方式，我经常能够将系统的约束表达为 ADT。

即ADT的所有可能值都是系统可能的状态，不存在不一致的范围。

情况总是如此，还是存在无法表示为 ADT 的约束？

(换句话说，当我无法将一组约束表示为 ADT 时，是否只是我看起来不够努力，或者某些类型的约束无法通过 ADT 执行？)

有数学证明吗？

---

更新:

这是一个玩具问题:

(roguelike)2D map 由方形单元组成，每个单元都有一种 Material (岩石或空气)。

每个像元有四个边界(N、S、E 和 W)。每个边界由两个单元共享。

仅当边界的一侧是岩石而另一侧是空气时，边界才可以选择包含“墙特征”。

(墙壁功能可以是控制杆、图片、按钮等)

当一侧是岩石而另一侧是空气时，什么 ADT 设计可以仅有地方存储墙壁特征？即数据结构不能表示两个空气单元或两个岩石单元之间边界上的壁特征。

Answer 1

对于状态数量有限的系统来说，这显然是正确的:

数据状态 = State1 |状态2 |状态3 |状态4 |状态5 | ...

但是状态数量非有限的系统又如何呢？如果我们限制自己编写有限的 Haskell 程序，那么只有可数多个 Haskell 程序，因此也只有可数多个 ADT。这是因为 Haskell 是一种用有限字母表编写的语言。

考虑以下数据类型，即位流:

data Stream = O Stream | I Stream

现在让我们开始写下一些可以表示为 Haskell 数据类型的流的随机约束。 (所有这些都必须可以表示为 Haskell 数据类型，或者在有限的 Haskell 程序中已经存在无法用 ADT 表示的类型):

Type 0 admits every stream except OIOIOIOO...
Type 1 admits every stream except IIOOOIOI...
Type 2 admits every stream except OOOIOIIO...
Type 3 admits every stream except OOOOIIIO...
Type 4 admits every stream except OOIOIOOO...
Type 5 admits every stream except OOIOOOIO...
Type 6 admits every stream except IIOIOIIO...
Type 7 admits every stream except IIIIIIIO...
...

我们最多可以在 Haskell 中写下可数个这样的数据类型，因为只有可数个有限的 Haskell 程序，并且每个有限的 Haskell 程序只能导出有限数量的没有类型变量的类型。使用类型变量导出类型的程序可能是创建类型为 Stream 约束版本的程序的有趣子程序，但由于 Stream 没有类型变量，所有这些类型显然都不是 Stream 的受限版本。 因此，如果我们可以证明存在无数种可能的数据类型，那么一定存在至少一种 Haskell ADT 无法准确表示的类型。

让我们继续写下数据类型，直到我们将它们全部写在有限 Haskell 程序可以表示的所有数据类型的无限列表中。由于这些数只有可数个，因此可以将它们映射到唯一的正整数以按顺序写下来。

现在，考虑以下数据类型。它承认每个流，除了以与类型 0 不允许的流相反的位开头的流之外，具有与类型 1 不允许的流的第二位相反的第二位，等等.

类型 x 允许除 IOIIOIOI 之外的所有流...

这称为康托对角线。

Type x isn't Type 0, because it admits anything that starts with an O, and the only thing Type 0 excludes is one stream that starts with an O
Type x isn't type 1, because it admits anything that has a second bit of I, and the only thing Type 1 excludes is one stream that has a second but of I.
Type x isn't type 2, because it admits anything that has a third bit if O, and the only thing Type 2 excludes is one stream that has a third bit of O.
...

事实上，类型 x 不是我们写下的任何数据类型，我们写下了有限 Haskell 程序可以表示的每一种数据类型，例如 Stream。因此，类型 x 不能由有限 Haskell 程序表示。