尧图建网站 尧图建网站 YAOTU WEB BUILD 免费咨询
ARTICLE DETAIL

资讯详情

深耕网站建设与建站编程的一线实战洞察。

OCaml 语法不支持直接定义受保护方法?用类型相等见证来实现!

OCaml 语法不支持直接定义受保护方法?用类型相等见证来实现! OCaml 中的受保护方法2025 年 6 月 29 日本文是一篇译文。受保护方法允许仅针对某些方法为接收器self添加约束即只有当接收器满足这些约束保护条件时这些方法才能被调用。OCaml 在语法上不允许直接定义这类方法本文将探讨如何使用类型相等见证来实现它们。问题呈现当一种在程序运行前进行类型检查的语言如 Java 或 OCaml引入参数多态Java 中的“泛型”时有时可对类型变量进行约束。例如通过假设类型变量 T 是 S 的子类型使 MyClass 成为泛型类。但这种约束适用于整个类有时我们希望约束仅适用于某些方法。比如对于描述列表的类 MyList若要定义 flatten 方法使列表 [[1, 2, 3], [4, 5]] 转换为 [1, 2, 3, 4, 5]在类级别设置约束会有很大局限性。为实现这样的方法有三种理论方法。将方法移出类第一种解决方案是将方法移出类体如移到静态上下文或伴生对象中。这种方法可行且无需特殊操作但要求开发者记录方法位置还破坏了向实例发送消息的系统性方法。扩展方法Kotlin 等语言提供了扩展方法它能扩展现有类在定义接收器方面更灵活。不过该解决方案仍要求方法在类外部定义可能需将类的某些成员设为 public存在潜在的抽象泄漏但保留了系统性的消息发送方法同时允许对接收器进行更细粒度的限定。受保护方法最后一种方法是受保护方法它将方法定义保留在类内部不会导致抽象泄漏。在假想语法中它能解决前面提出的问题如可更精确描述接收器、不破坏常规消息发送、不会出现表示泄漏。但遗憾的是主流语言中没有一种允许定义它们幸运的是在 OCaml 中可以对它们进行编码。OOP/FP 对称性理论与实践受保护方法在流行编程语言中罕见作者在阅读 Gabriel Scherer 的演讲“面向对象编程与函数式编程的对称性理论与实践”的幻灯片时发现了它们。该演讲展示了静态类型函数式编程工具与面向对象编程工具之间的对称性虽这种对称性已被多次研究但该演讲全面且易于理解。演讲中未涉及受保护方法但幻灯片中有相关完整章节原始示例展示了经典函数式风格的 flatten 函数实现与面向对象世界中 flatten 方法实现之间的对称观察。Gabriel Scherer 提出的语法可描述受保护方法但遗憾的是这种语法在 OCaml 中不可用不过我们可以使用一些小工具来对其进行编码。OCaml 中的受保护方法作者在遇到一些特殊情况后向 OCaml 社区的 Florian AngelettiOctachron求助。我们的目标是为某些方法添加约束在不修改语言语法的情况下可通过提供额外参数来强制执行约束即提供证据。提供类型相等见证自从 OCaml 引入广义代数数据类型以来有一种直接的方法定义类型相等见证即定义 eq 类型它只有一个构造函数 Refl可表示类型检查器未知的类型相等性。在一个作用域内实例化 Refl 可保证类型等价。有些情况下编译器无法知道类型相等如运行时提供数据或类型表示被抽象隐藏时。若能构造 Refl 值就可保证两个语法上不同的类型实际上相等。使用 eq 进行约束回到为列表提供对象 API 的例子其接口为 obj_list。为给 flatten 方法指定类型需证明 a 的类型是 b list即保证 a 和 b list 相等只需提供类型为 (a, b list) eq 的值。实现 obj_list 接口前几个方法length、append 和 uncons容易实现重点关注 flatten 方法它将递归遍历列表并连接元素关键在于实例化 Refl 提供 a b list 的证据。添加受保护方法 sum我们尝试添加 sum 方法计算整数列表总和将 sum 方法添加到接口中用 (a, int) eq 作为类型相等见证。实现 sum 方法只是对 fold_left 函数的使用。可以对不同类型的对象调用不同方法若对错误类型的对象应用受保护方法程序将无法编译这正是预期行为。现在我们可以通过类型相等见证来定义约束接收器类型的方法任务完成总结并非所有静态类型的面向对象语言都支持受保护方法它们能在保留面向对象编程消息传递语义的同时表达更多方法。作者不太了解哪些语言提供对受保护方法的语法支持最近得知 Scala 语言使用类似编码方式类型相等见证是隐式提供的简化了调用。尽管这种编码方式繁琐但显式操作类型相等见证使我们能够对它们进行编码。在 OCaml 中很少鼓励使用面向对象编程可能不太有用但展示一个具体且实际的相等见证用例仍然很有趣
返回列表