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

发布时间：2020-12-13 20:46:37 所属栏目：百科来源：网络整理

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

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

function loadStudent(studentId: Integer) : Student

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

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

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

也许我误解了这个问题,但我不知道如果不做IO就可以做到这一点.如何在不搜索数据库的情况下知道id是否有效,以查看是否存在具有该id的记录？

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

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

（编辑：李大同）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!