问题标签 [locally-abstract-type]

我目前正在使用模块，看看它们可以以与 Haskell 类型类类似的方式使用。目前我正在尝试使用仿函数类型类：

但是，在这种情况下outmap将无法正确键入，编译器会产生错误The type constructor F.f would escape its scope。我知道为什么在这种情况下会导致此错误，但我不确定如何解决它（因为类型 f 已参数化）。

我已经尝试使用本地抽象类型：

或者

或者

这一切都只是给我各种语法错误或打字错误。

有没有办法解决这个问题？

在 Haskell 中，这只是：

ocaml 中的等价物（如果有的话）是什么？

==== 编辑 ====

我找到了一种类似于工作的方法：

但这看起来增加了很多复杂性，因为这可能应该更简单。

我刚刚在OCaml 关于 GADTs 的文档中遇到了以下代码片段：

在 utop 中评估后，它具有以下签名：

我还注意到，当替换type a. a term -> a或'a term -> 'a仅删除签名时，该函数不再编译。

那么这个符号是什么？是什么让它与众不同'a t？

它是否特定于 GADT？

有没有办法在类型上对模块进行参数化或从 OCaml 中的模块中转义类型？基本上，我想编写一些在浮点类型上参数化的例程，并且仍然可以访问 (+.)、(-.) 等运算符。当然，我们可以编写一个浮点模块，例如

它对普通浮点数有一个非常基本的实现

然后，我尝试在带有代码的模块中本地使用此模块

这个函数有我想要的类型

但是，如果我运行它，编译器会抱怨

当然，我们可以使用模块中的注入功能

但结果类型是抽象的，而不是浮点数。最终，我想要一种让函数 double 返回公开类型的方法。如果可能的话，我不想使用 REAL 模块中的另一个函数来转换t->float. t我希望以某种方式暴露实际类型。另外，我想通过在本地使用模块而不是在REAL.

在ocaml 手册第 7.20 节中的 GADT 基本示例中，“类型 a”的含义是什么。? 为什么声明“eval : a term -> a”是不够的？

GADT 允许某种形式的动态类型：

我希望能够进行相同类型的调度，但使用参数化类型，并且可以从外部访问 gadt 的参数。如果参数被普遍量化或固定，这很容易：

但是，如果参数上有其他形式的约束，则此方法不起作用：

我得到了错误：类型构造函数 a#0 会逃脱它的作用域。我想这是由于外部限制，没有完全了解领域。

我发现的唯一解决方案是使用 Higher 模块：

然而，这个解决方案远非完美：首先它很冗长，到处都有 inj 和 prj，更重要的是，它有很多限制：'a 参数不能有约束，也不能有方差......

有人知道更好的解决方案吗？

编辑

经过一番思考，Drup 解决方案是有效的，但必须小心！在我的完整问题（不是这个问题中的玩具程序）中，我需要在方法定义中访问 self 。所以回到 Drup 解决方案，我必须将 self 传递给中间函数，为此，我必须给它一个类型。所以我必须首先声明一个类类型......

但是，如果类c对'a: 的类型有限制，这将不起作用cons，因为a必须普遍量化但在a c_type. c_type解决方案是在没有约束的情况下编写'a. 但是请注意，这意味着大量的重写。在许多情况下，仅仅省略约束不足以使其消失：它的所有用法都必须是无约束的......

所以最终的解决方案如下：

我试图弄清楚如何根据具有参数类型的模块编写函数，但我在任何地方都找不到类似的东西。我试图尽可能地减少问题并最终得到这个虚拟示例。

这会产生错误Error: Syntax error: module-expr expected。

如果我放弃'a，我最终会出现以下错误。

这样做的正确语法是什么？

我正在尝试建模“异构树”，即。一棵树，其中节点具有不同的“种类”，并且每个“种类”都被限制在它们可能包含的子“种类”中：

然后可以像这样定义树：

通常这将使用每种“类型”节点的单独变体来完成，但我试图将其定义为 GADT，以便能够使用模式匹配每种节点的高阶函数来操作树：

我遇到的问题是定义接受上述高阶函数并将其应用于每个节点的函数。到目前为止，我有这个：

但是编译器在突出显示的行上给了我以下错误

这个表达式的类型是块节点 -> 一个节点选项，但是一个表达式应该是类型块节点 -> 一个节点选项这个块的实例是模棱两可的：它会逃脱其方程的范围

或者，如果我将类型更改为，则会f收到'a node -> 'a node option此错误

此表达式具有节点类型，但表达式应为节点类型 类型构造函数 a 将逃脱其范围

显然，我并不完全理解本地抽象类型（或真正的 GADT，就此而言），但据我所知，这些错误似乎出现了，因为该类型，顾名思义，是“本地的”，而在在外面，传递它会“泄漏”它，我猜？

所以我的问题是，首先是：这甚至可能做到吗（并且“这个”我认为我的意思是在高阶函数中对 GADT 进行模式匹配，但我什至不确定这是实际问题） ?

所有代码都在这里的游乐场

我正在为具有两种可能的内部格式的矩阵类型编写接口。这是一个简化版本：

这不起作用，因为默认值CSC不是 type s fmt。

看来这个想法是没有机会了，因为无法在签名中指定类型变量的默认值，也就是签名

会以某种方式需要指定's = csc何时fmt未明确指定。

有没有办法绕过这个限制？

期望 OCaml 接受这样的定义是不合理的吗？

我仍在试图弄清楚在使用 mirage 时如何拆分代码，它有无数的一流模块。我已经把我需要的一切都放在了一个又大又丑的Context模块中，以避免将十个模块传递给我的所有功能，一个就够痛苦了。

我有一个通过 tcp 接收命令的功能：

经过数小时的反复试验，我发现我需要添加(type a)“显式”type chan = a才能使其工作。看起来很难看，但它可以编译。但是，如果我想让该函数递归：

我通过了两次模块，第一次没问题，但在递归行上出现错误：

如果我尝试指定我得到的签名

似乎我不能使用整个(type chan = a)东西。如果有人可以解释正在发生的事情，以及理想的解决方法，那就太好了。我当然可以使用一段时间，但我宁愿最终理解这些该死的模块。谢谢 ！

我想在本地存储的数据集上过滤关于 Corona 的最常见/最受欢迎的推文（比如最被转发的推文）。但如果我使用：

它总是试图查看 Twitter 本身。

与

或者

什么都没发生