database - 使用依赖类型来提供编译类型证明某个整数是数据库中的有效行 ID？

Question

在我对依赖型土地永无止境的奇迹中，一个奇怪的想法出现在我的脑海中。我做了很多数据库编程，如果我能摆脱所有那些健全性检查和有效性检查，那就太好了。一个特别烦人的情况是那些接受 Integer 并期望它是某个特定表的有效行 ID 的函数。一个非常愚蠢的例子是：

function loadStudent(studentId: Integer) : Student

假设我选择的语言完全支持依赖类型，是否可以利用类型系统loadStudent只接受有效值studentId：

function loadStudent(studentId : ValidRowId("students_table") ) : Student

如果是，我如何为ValidRowId类型编写数据构造函数？到目前为止，我看到的所有示例都是纯的（不涉及 IO）。

Answer 1

也许我误解了这个问题，但我不明白不做 IO 怎么可能。如果不搜索数据库以查看是否存在具有该 id 的记录，您如何知道该 id 是有效的？

我想您可以在程序启动时将所有当前 ID 读入内存中的表中，然后对此进行检查。但是您必须以某种方式知道其他用户在您创建表后是否添加或删除了记录。

好的，您可以让访问数据库的所有计算机上的所有线程与某个中央服务器通信，该服务器保留此主列表，以便它始终是最新的。但是我们已经有一个中心位置来跟踪数据库中当前使用的所有 ID：它被称为“数据库”。做一大堆工作来维护数据库上数据子集的副本有什么好处？您不太可能获得很大的性能提升，并且您可能会创建代码中的错误、不良连接等导致数据不同步的可能性。