我正在开发一个基于some existing code 的项目，该项目使用unbound 库。
代码使用unsafeUnbind 一堆，这给我带来了问题。
我尝试过使用freshen，但出现以下错误：
error "fresh encountered bound name!
Please report this as a bug."
我想知道：
FreshM monad 中使用？或者他们是否可以在不进入Fresh 的情况下执行 lambda 应用程序之类的事情？freshen 什么样的值，以避免他们列出的错误？unsafeUnbind，在什么条件下可以安全使用？【问题讨论】：
标签： haskell scope lambda-calculus
该库是否打算完全在
FreshM monad 中使用？或者他们有没有在Fresh中做诸如 lambda 应用之类的事情的方法？
在大多数情况下，您会希望在 Fresh 或 LFresh monad 中进行操作。
我可以给
freshen什么样的值，以避免他们列出的错误？
所以我认为您收到错误的原因是因为您将 term 传递给 freshen 而不是 pattern。在 Unbound 中，模式就像是名称的概括：单个 Name E 是由一个代表 Es 的变量组成的模式，但 (p1, p2) 或 [p] 是由一对模式 @ 组成的模式分别为 987654332@ 和 p2 或模式列表 p。例如，这使您可以定义同时绑定两个变量的术语。其他更奇特的类型构造函数包括 Embed t 和 Rebind p1 p2 前者创建一个在模式内嵌入术语的模式，而后者类似于 (p1,p2) 除了 p1 范围内的名称超过 p2 （对于例如，如果p2 中有Embeded 条款，p1 将是这些条款的范围）。这真的很强大，因为它可以让你定义像 Scheme 的 let* 形式，或者像依赖类型语言中的 telescopes 这样的东西。 （详见论文）。
最后，类型构造函数Bind p t 将术语和类型结合在一起：术语Bind p t 意味着p 中的名称绑定在Bind p t 中，并且范围超过t。因此，可以使用data Expr = Lam (Bind Var Expr) | App Expr Expr | V Var 其中type Var = Name Expr 构造一个（无类型的）lambda 项。
所以回到freshen。你应该只在 patterns 上调用freshen，所以在Bind p t 类型的东西上调用它是不正确的（我怀疑你看到的错误消息的来源） - 你应该只调用它p，然后将生成的排列应用于术语 t 以应用 freshen 构造的重命名。
如果我最终使用 `unsafeUnbind，在什么条件下可以安全使用？
我使用它的地方是如果我需要暂时潜入活页夹并执行一些我知道肯定不会对名称做任何事情的操作。一个例子可能是从一个术语中收集一些源位置注释，或者用一个封闭的术语替换一些全局常量。此外，如果您可以保证您正在使用的术语已经被重命名，那么您 unsafeUnbind 的任何名称都将是唯一的。
希望这会有所帮助。
PS：我维护 unbound-generics，它是 Unbound 的克隆，但使用 GHC.Generics 而不是 RepLib。
【讨论】：