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

Question

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

function loadStudent(studentId: Integer) : Student

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

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

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

Answer 1

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

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

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