是否可以在 OCaml 中进行编译时执行,类似于 C++模板元编程?
在 C++ 中,递归模板和常量值作为模板参数允许执行有趣的代码生成和编译时执行示例,例如 阶乘。
是否可以使用参数多态性、函子或其他概念在 OCaml 中执行类似的操作?
In C++, recursive templates and constant values as template parameters allows to do interesting examples of code generation and compile-time execution, such as the factorial.
Is it possible to do similar things in OCaml, using parametric polymorphism, functors, or other concepts?
如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱,如果其他用户或者作者回复了您的评论,将不能在第一时间通知您!
发布评论
评论(2)
ocaml干扰系统使用统一。你可以把它看作一个计算设备,在这种情况下它有一种逻辑编程的感觉。但可能性相当有限,因为这从来都不是类型系统的目标之一。正如您将在 Jeffrey 建议的页面中看到的那样,通过统一进行的类型级计算实际上相当有限(很难表达,例如乘法)。 Haskell 有更强大的约束语言,但我再次不确定类型系统中的逻辑编程是否是一个好方法。
OCaml 类型系统可以进行类型级计算的另一部分是在其模块和函子语言中。函子允许以与正式编程语言 Fω 相关的风格来表达类型级计算。您可能可以在模块语言的类型级别对教堂数字进行编码,但我不知道您可以用它做什么,因为以有用的、可利用的形式检索结果似乎相当困难。特别是,我不知道如何将该类型信息转换回程序可用的值,就像 C++ 或 D 对其编译时常量计算所做的那样。
所以,是的,OCaml 的类型系统(以及大多数函数式语言,也包含 SML、Haskell 和 Scala)具有一定的计算能力,但不,我不希望这样做特别有用与它们进行预计算;这当然不是 OCaml 程序员的标准做法。类型最好被视为类型,它为它们分类的值带来静态保证。
The ocaml inteference system uses unification. You can consider it a computational device, and in this case it has a feeling of logic programming. But the possibilities are rather restricted as this was never one of the goals of the type system. As you will see in the page suggested by Jeffrey, type-level computations through unification are actually rather limited (hard to express eg. multiplication). Haskell has a more powerful constraint language, abut again I'm not sure logic programming in the type system is a good way to go.
The other part of the OCaml type system can do type-level computation is in its module and functor language. Functors allow to express type-level computations in a flavor that has been linked to the formal programming language Fω. You could probably encode church numerals at the type level in the module language, but I don't see what you could do with this, as it is seems quite difficult to retrieve the results in an useful, exploitable form. In particular, I don't see how to turn that type information back into values usable by your program, as C++ or D do with their compile-time constant computation.
So yes, the type system of OCaml (and most functional language, that would hold of SML, Haskell and Scala as well) has some computational strength, but no, I wouldn't expect to do particularly useful pre-computation with them; and it's certainly not standard practice among OCaml programmers. Types are best seen as types, that bring static guarantees about the values they classify.
您可以在 OCaml 类型系统中进行算术运算;一个非常简单的例子出现在这个
其他 Stackoverflow 页面:
我想你可以使用这种机制来计算类型中的阶乘系统。如果您使用数字的标准一元(Peano)编码,一旦数字开始变大,结果将非常可怕。所以这只是一个有趣的噱头。
如果你想在类型级别看到真正有趣的计算,你应该看看 Haskell。一些常见的扩展(在 GHC 中可用)允许在类型系统中进行任意计算。即,类型系统是图灵完备的。
You can do arithmetic in the OCaml type system; a very simple example appears on this
other Stackoverflow page:
I imagine you could use this mechanism to calculate factorials in the type system. If you use the standard unary (Peano) encoding of numbers, the results are pretty ghastly once the numbers start to get big. So it would just be an interesting stunt.
If you want to see really interesting computations at the type level, you should look at Haskell. Some common extensions (available in GHC) allow arbitrary computations in the type system. I.e., the type system is Turing complete.