Unbound总是需要在`FreshM` monad中吗？

Question

我正在基于一些使用未绑定库的现有代码开发项目.

代码使用unsafeUnbind了一堆,这导致我的问题.

我尝试过使用freshen,但是我收到以下错误:

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

我在想:

• 该库是否打算完全在FreshMmonad中使用？或者他们的方式来做lambda应用程序而不是在做Fresh什么？
• 我可以给出什么样的价值freshen,以避免他们列出的错误？
• 如果我最终使用unsafeUnbind,在什么条件下使用是否安全？

Answer 1

该库是否完全用于FreshM monad？或者他们的方式来做lambda应用程序而不是在做Fresh什么？

在大多数情况下,您需要在a Fresh或LFreshmonad中操作.

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

所以我觉得你得到了错误的原因是因为你传递一个术语来freshen,而不是一个模式.在未结合的,图案等名称的概括:单Name E是由它代表单个变量的图案ES,而且(p1, p2)或者[p]是由一对的图案的图案p1和p2或的模式的列表p,分别.例如,这允许您定义同时绑定两个变量的术语.其他更奇特的类型构造函数包括Embed t和Rebind p1 p2前者创建一个模式,在模式中嵌入一个术语,而后者类似于(p1,p2)除了p1范围内的名称p2(例如,如果在其中p2有Embeded术语,p1将是这些术语的范围) .这非常强大,因为它可以让你定义像Scheme的let*形式,或像依赖类型语言的望远镜.(详见论文).

现在终于类型构造Bind p t是什么让一个术语和类型一起:一个术语Bind p t意味着在名称p在约束Bind p t和范围上t.因此,(无类型的)lambda术语可以用data Expr = Lam (Bind Var Expr) | App Expr Expr | V Varwhere 构造type Var = Name Expr.

所以回到freshen.您应该只调用freshen上的模式,以便调用它的类型的东西Bind p t是不正确的(我怀疑你看到的错误消息的来源) -你应该调用它只是p然后将得到的置换适用于术语t应用重命名该freshen构造.

如果我最终使用`unsafeUnbind,在什么条件下使用它是安全的？

我使用它的地方是,如果我需要暂时潜入一个活页夹,并做一些我知道肯定对名称没有任何操作的操作.一个例子可能是从一个术语中收集一些源位置注释,或者用一个封闭的术语替换一些全局常量.此外,如果您可以保证已经重命名了您正在使用的术语,那么任何您unsafeUnbind将成为唯一的名称.

希望这可以帮助.

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