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

Question

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

function loadStudent(studentId: Integer) : Student

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

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

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

Answer 1

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

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

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