数据和状态的所有约束都可以表示为代数数据类型吗？
我喜欢我经常能够将系统约束表达为 ADT 的方式。
即 ADT 的所有可能值都是系统的可能状态，没有不一致的余地。
是否总是如此，或者是否存在不能表示为 ADT 的约束？
（换句话说，当我无法将一组约束表示为 ADT 时，仅仅是我不够努力，还是某些类型的约束无法通过 ADT 执行？）
有这方面的数学证明吗？
更新：
这是一个玩具问题：
（roguelike）2D 地图由方形单元组成，每个单元都有一种材料（岩石或空气）。
每个单元格有四个边界（N、S、E 和 W）。每个边界由两个单元共享。
仅当一侧是岩石而另一侧是空气时，边界才可以选择包含“墙特征”。
（墙壁特征可以是杠杆、图片、按钮等）
只有当一侧是岩石而另一侧是空气时，什么 ADT 设计才能有一个存储墙壁特征的地方？即数据结构不能表示两个空气单元或两个岩石单元之间边界上的壁特征。
对于具有有限数量状态的系统来说，这显然是正确的：
数据状态 = 状态 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.
...
事实上，Type x 不是我们写下的任何数据类型，我们写下每一种数据类型，就像Stream一个有限的 Haskell 程序可以表示的那样。因此类型 x 不能用有限的 Haskell 程序表示。