我可以为某些函子参数定义OCaml函数吗？

我愿做这样的事情：我可以为某些函子参数定义OCaml函数吗？

module Make (M: MInt) (N: MInt) : T = struct 
    (* always defined *) 
    let foo = 42 

    (* only defined when M == N or M.x == N.x, something like that *) 
    let bar a b = a * b 
end

这可能吗？

显然我可以在运行时检查，但我很好奇如何在编译时做到这一点。谢谢！

来源

2015-08-09 jenga

要编码这种类型的东西，需要使用dependent typing的语言。依赖打字是类型系统的一个强大功能，但不幸的是，它使语言复杂化并使类型推断不可判定。通常情况下，这比平均程序员愿意支付更多。如果你真的想要一种能够让你编写这样的规范的语言，那么你需要尝试Coq。

OCaml仍然支持通过Generalized Algebraic Data types来限制从属打字。因此，从理论上讲，在OCaml中，您可以编码一个函数，该类型可确保两个参数是相等的整数。为此，您需要使用Peano数字而不是内置整数，或者使用幻像类型对内置整数进行注释，描述其大小。但是这一切都是不切实际的。在Coq中编写这些代码要容易得多，然后将该定义提取为OCaml程序。

总而言之，不可能在函子级别上做你想要的。用OCaml类型系统表达这样的东西是可能的。但为此，最好使用Coq，并在OCaml中保持简单。

来源

2015-08-09 15:40:20 ivg

不，我不相信函数的结果模块的字段列表（签名）可能以这种方式依赖于参数模块。我认为唯一可以得到的依赖是类型替换。

来源

2015-08-09 11:54:31 antron

你可以有延伸的第一，但需要的模块等于第二函子：

module Make (M: MInt) (N: MInt) : T = struct 
    let foo = 42 
end 

module Make2 (M: MInt) : T2 = struct 
    include Make(M)(M) 

    let bar a b = a * b 
end

来源

2015-08-10 14:44:28

我可以为某些函子参数定义OCaml函数吗？

回答

相关问题