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

Question

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

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

即ADT 的所有可能值都是系统可能的状态，没有不一致的余地。

总是这样，还是有不能表示为 ADT 的约束？

（换句话说，当我无法将一组约束表示为 ADT 时，是我不够努力，还是某些类型的约束无法通过 ADT 执行？）

有这方面的数学证明吗？

---

更新：

这是一个玩具问题：

（roguelike）2D 地图由方形单元组成，每个单元都有一种材料（岩石或空气）。

每个单元格有四个边界（N、S、E 和 W）。每个边界由两个单元格共享。

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

（墙壁特征可以是杠杆、图片、按钮等）

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

Answer 1

这对于具有有限数量状态的系统显然是正确的：

数据状态 = 状态 1 |状态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 程序表示。