Obj 模块文档

发布于 2024-11-07 19:07:19 字数 183 浏览 1 评论 0原文

有关于 Obj 模块的任何文档吗?我只能找到没有任何描述的函数列表 ...

(顺便说一句:我知道这些是低级函数,不适合普遍使用)

Is there any documentation about the Obj module? I could only find a list of functions without any description...

(BTW: I know these are low-level functions not meant to be generally used)

如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。

扫码二维码加入Web技术交流群

发布评论

需要 登录 才能够评论, 你可以免费 注册 一个本站的账号。

评论(3

一指流沙 2024-11-14 19:07:19

是的,这显然是故意没有记录的。对于 Obj 的五种用途,我看到(或者我自己写,这更令人不安),其中两种是不合理的,其中两种是避免更干净的设计更改的方法,无论如何,这都是有用的,并且其中之一是对复杂问题的真正“好解决方案”。

Obj 仅公开允许探索和操作 OCaml 数据的运行时表示的类型破坏操作。您不需要这些函数的文档,它们很明显,但您需要了解 OCaml 数据表示(我使用 此文档,但是 ocaml 手册也记录了它),如果你想破解它你应该了解运行时,以了解什么是安全的,什么是不安全的。一般来说:不要。

以下是 Obj 的一些合法用途:

  • Coq 程序编译为 OCaml 程序时; Coq 类型系统更强大,它可以输入 OCaml 会拒绝的内容,因此 Coq->Ocaml 翻译器插入 Obj.magic 调用以强制 OCaml 接受其输出。

  • 在 OCaml 3.x 中编码 GADT 时,该版本不支持它 - 它们被添加到 4.00 中。有一种具有模块级相等性和函子的编码(请参阅这篇文章这项工作),但更常见的一个(在 menhir 解析器生成器,它是 ocamlyacc 的一个很好的替代品,请参阅 本文 (PDF)) 使用Obj.magic

  • 当使用某种(自制的)运行时类型信息编组数据时。 OCaml 的 Marshal 模块已经不是类型安全的(出于明显的原因),并且如果您需要在不同的上下文中进行不同类型的编组(例如,到/从 SQL 服务器的查询和结果) ,正如我在我的 macaque 项目中所做的那样),您将需要某种不安全的强制转换。

Yes, it is clearly undocumented on purpose. For five uses of Obj I see (or write myself, which is more disturbing), two of them are unjustified, two of them are a way to avoid a cleaner design change that would be useful anyway, and one of them is a genuine "good solution" to a complicated problem.

Obj only expose type-breaking operations that allow to explore and manipulate the runtime representation of OCaml data. You don't need documentation for these functions, they're obvious, but you need to know about OCaml data representation (I learned it using this document, but the ocaml manual also documents it), and if you want to hack into it you should know about the runtime to know what's safe and what isn't. As a general rule: don't.

Here are a few legitimate uses of Obj:

  • when compiling Coq programs to OCaml programs; the Coq type system being more powerful, it can type things that OCaml would reject, hence the Coq->Ocaml translator inserts Obj.magic calls to force OCaml into accepting its output.

  • when encoding GADTs in OCaml 3.x, which didn't support it -- they were added to 4.00. There is one encoding with module-level equality and functors (see this post or this work), but the more common one (used in the menhir parser generator which is a great replacement for ocamlyacc, see this paper (PDF)) uses Obj.magic

  • when marshalling data using some kind of (home-made) runtime type information. The Marshal module of OCaml is already not type-safe (for obvious reason), and if you need a different kind of marshalling in a different context (eg. to/from queries and results for a SQL server, as I did in my macaque project) you will need some kind of unsafe cast.

隐诗 2024-11-14 19:07:19

模块 Obj 基本上处理堆中 OCaml 值的结构和解释。如果您想了解这意味着什么,您必须阅读 OCaml 手册的第 18 章,“C 与 Objective Caml 的接口”。

没有记录的原因有两个:首先,这些函数非常不安全。根本没有没有类型为 'a ->; 的完整函数。 'b 因此您可以看到,如果 Obj.magic 要返回任何内容,它必须执行相当多的操作。事实上,它只是类型系统中的一个漏洞,一个“杀死它的许可证”。其次,该模块允许您随意查看堆,实际上提供了 C 的 void 指针的道德等价物。这与不受限制的强制转换相结合,让您可以从 OCaml 做任何您想做的事情。

不过,Obj 有合法用途。我统计了源代码中 Obj.magic 的出现次数超过 100 次,尤其是在 PrintfScanf 的代码中。另一个合法用途是尾递归列表操作,只要您可以证明代码是类型安全和线程安全的

如果您不介意自插,这里有一个示例 包含在安全接口中的不安全操作,以及证明(“因为每一步 cons 单元都是新鲜的......”)它确实是安全的,并且 这是另一个

The module Obj basically deals with the structure and interpretation of OCaml values in the heap. If you want to understand what this means you must read chapter 18 of the OCaml manual, "Interfacing C with Objective Caml".

The reason why this is undocumented is twofold: first of all, the functions are horribly unsafe. There is simply no total function with type 'a -> 'b so you can see that Obj.magic must do quite a bit of it if it is to return anything at all. In fact it is just a hole into the type system, a "license to kill" it. Second, the module allows you to peek and poke into the heap at will, in effect providing the moral equivalent of C's pointers to void. This together with unrestricted casts lets you do whatever you want from OCaml.

There are legitimate uses for Obj, though. I count more than 100 occurrences of Obj.magic in the sources, most notably in the code for Printf and Scanf. Another legitimate use is for tail-recursive list operations, provided you can prove that the code is type-safe and thread-safe.

If you don't mind the self-plugs, here is an example of an unsafe operation that is wrapped in a safe interface, together with a proof ("Since at each step the cons cell is fresh…") that it is indeed safe, and here is another.

分分钟 2024-11-14 19:07:19

您找不到这些函数的任何文档。如果你想使用它们,我不会重复说这是不鼓励的,你必须阅读并理解它们的实现。但据我记得,其中三个是作为“%identity”实现的,所以这并不像看起来那么难。

You won't find any documentation for these functions. If you want to use them, and I won't repeat that this is discouraged, you have to read and understand their implementation. But as I remember, three of them are implemented as "%identity", so this is not as hard as it seems.

~没有更多了~
我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站,即表示您同意使用 Cookies 和您的相关数据。
原文