Unbound是否總是需要在`FreshM` monad中？

Question

我正在使用基於some existing code的項目，該項目使用unbound庫。

該代碼使用unsafeUnbind一堆，這是我的問題。

我使用freshen試過，但我得到以下錯誤：

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

我想知道：

• 將是一個FreshM單子內完全使用意庫？還是他們的方式來做像lambda應用程序這樣的事情，而不是在Fresh？
• 我可以給freshen什麼類型的值，以避免他們列出的錯誤？
• 如果我最終使用unsafeUnbind，在什麼情況下可以安全使用？

Answer 1

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

在大多數情況下，你會想一個Fresh或LFresh單子內運行。

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

所以我認爲你得到錯誤的原因是因爲你傳遞一個長期到freshen而非模式。在未結合的，圖案等名稱的概括：單Name E是由它代表E秒的單可變的圖案，但也(p1, p2)或[p]是由一對圖案p1和p2或圖案p列表的模式， 分別。例如，這可讓您定義同時綁定兩個變量的術語。其他更奇異的型構造包括Embed t和Rebind p1 p2前者使嵌入的圖案的內部的術語的圖案，而後者則是類似於(p1,p2)不同之處在於在p2p1範圍內的名稱（例如，如果p2中有Embed編方面， 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 Var來構造，其中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。