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 ?
Dans la plupart des situations que vous voulez utiliser dans un Fresh ou un LFresh monade.
What kinds of values can I give to freshen , in order to avoid the errors they list?
Je pense donc la raison pour laquelle vous obtenez l'erreur est parce que vous passez un terme -freshen plutôt qu'un motif . En Unbound, les modèles sont comme une généralisation des noms: un Name E unique est un modèle constitué d'une seule variable qui signifie E s, mais aussi (p1, p2) ou [p] sont des modèles constitués d'une paire de motifs p1 et p2 ou une liste de motifs p , respectivement. Cela vous permet de définir des termes qui lient deux variables en même temps, par exemple. D'autres constructeurs de types plus exotiques comprennent Embed t et Rebind p1 p2 ancien fait un modèle qui intègre un terme à l'intérieur d'un motif, alors que celui-ci est similaire à (p1,p2) sauf que les noms dans p1 portée plus p2 (par exemple, si p2 a Embed termes ées en elle, p1 sera portée sur ces termes). Ceci est vraiment puissant car il vous permet de définir des choses comme le formulaire let* de Scheme, ou télescopes comme dans les langues typées en fonction. (Voir le document pour plus de détails).
Maintenant, enfin, le constructeur de type Bind p t est ce qui apporte un terme et un type ensemble: Un terme Bind p t signifie que les noms p sont liés à Bind p t et la portée sur t. Ainsi, un terme lambda (non typé) peut être construit avec data Expr = Lam (Bind Var Expr) | App Expr Expr | V Var où type Var = Name Expr.
Retour à freshen. Vous devez appeler uniquement freshen sur les modèles donc l'appeler sur quelque chose de type Bind p t est incorrect (et je soupçonne la source du message d'erreur que vous voyez) - vous devriez l'appeler seulement le p, puis appliquer la permutation résultante à le terme t pour appliquer le renommage que freshen construit.
If I end up using `unsafeUnbind, under what conditions is it safe to use?
L'endroit où je l'ai utilisé est si je dois partir furtivement temporairement sous un liant et faire une opération que je sais ne vous fait rien pour les noms. Un exemple pourrait consister à collecter certaines annotations de position source à partir d'un terme ou à remplacer une constante globale par une expression fermée. Aussi, si vous pouvez garantir que le terme avec lequel vous travaillez déjà a été renommé, tous les noms que vous allez unsafeUnbind seront déjà uniques.
Espérons que cela aide. PS: Je maintiens unbound-generics qui est un clone de Unbound, mais en utilisant GHC.Generics au lieu de RepLib.