haskell - Unbound 是否总是需要在 `FreshM` monad 中？

Question

我正在开发一个基于 some existing code 的项目使用 unbound图书馆。

代码使用 unsafeUnbind一堆，这给我带来了问题。

我试过使用 freshen ，但我收到以下错误:

error "fresh encountered bound name! 
Please report this as a bug."

我在想:

该库是否打算完全在 FreshM 中使用？单子(monad)？或者他们是否可以在不进入 Fresh 的情况下执行 lambda 应用程序之类的事情？ ?

我可以给 freshen 什么样的值，以避免他们列出的错误？

如果我最终使用 unsafeUnbind ，在什么条件下可以安全使用？

Answer 1

Is the library intended to be used entirely within a FreshM monad? Or are their ways to do things like lambda application without being in Fresh?

在大多数情况下，您会希望在 Fresh 内进行操作。或 LFresh单子(monad)。

What kinds of values can I give to freshen, in order to avoid the errors they list?

所以我认为您收到错误的原因是因为您将一个术语传递给 freshen而不是一种模式。在 Unbound 中，模式就像名称的概括:单个 Name E是由一个变量组成的模式，它代表 E s，还有 (p1, p2)或 [p]是由一对模式组成的模式 p1和 p2或模式列表 p ， 分别。例如，这使您可以定义同时绑定(bind)两个变量的术语。其他更奇特的类型构造函数包括 Embed t和 Rebind p1 p2前者创建一个在模式内嵌入术语的模式，而后者类似于 (p1,p2)除了 p1 中的名称范围超过 p2 (例如，如果 p2 中有 Embed ed 条款， p1 将是这些条款的范围)。这真的很强大，因为它可以让你定义像 Scheme 的 let* 这样的东西。形式，或者像依赖类型语言那样的望远镜。 (详见论文)。

现在终于类型构造函数 Bind p t是将术语和类型结合在一起的原因:术语 Bind p t表示 p 中的名称绑定(bind)在 Bind p t和范围超过 t .因此，可以使用 data Expr = Lam (Bind Var Expr) | App Expr Expr | V Var 构造一个(无类型的)lambda 项。在哪里 type Var = Name Expr .

所以回到 freshen .您应该只调用 freshen在模式上调用它类型为 Bind p t不正确(我怀疑您看到的错误消息的来源) - 您应该只在 p 上调用它然后将得到的排列应用于术语 t应用重命名 freshen结构体。

If I end up using `unsafeUnbind, under what conditions is it safe to use?

我使用它的地方是如果我需要暂时潜入活页夹并进行一些我知道肯定不会对名称做任何事情的操作。一个例子可能是从一个术语中收集一些源位置注释，或者用一个封闭的术语替换一些全局常量。此外，如果您可以保证您正在使用的术语已经被重命名，那么您 unsafeUnbind 的任何名称已经是独一无二的了。

希望这可以帮助。

PS:我维护 unbound-generics这是 Unbound 的克隆，但使用 GHC.Generics 而不是 RepLib。