[Haskell-cafe] Unbound: rebind and unrebind
Eric Dobson
eric.n.dobson at gmail.com
Sun Apr 14 19:57:43 CEST 2013
I am working at reimplementing the library Unbound to understand how
it works. One issue I have come up with is that an equation that I
thought held true doesn't. The equation is: Forall e::Rebind a b, e
`aeq` (uncurry rebind . unrebind $ e) => True. That is that spliting
the binding of a rebind and then adding it back should be the
identity. The issue is that Rebind does not freshen its pattern
variables on unrebind, because it assumes that a higher level unbind
already did that if required. But I believe this is not sufficient as
there is not necesarily a higher level Bind to be ubound as shown by
this program:
{-# LANGUAGE TemplateHaskell, UndecidableInstances,
FlexibleInstances, MultiParamTypeClasses #-}
module Main where
import Unbound.LocallyNameless
data Exp = Var (Name Exp) deriving Show
$(derive [''Exp])
instance Alpha Exp
instance Subst Exp Exp where
isvar (Var x) = Just (SubstName x)
x :: Name Exp
x = string2Name "x"
y :: Name Exp
y = string2Name "y"
rebindPass :: Alpha a => Rebind Exp a -> Rebind Exp a
rebindPass = (uncurry rebind . unrebind)
main :: IO ()
main = do
let rebound = (rebind (Var y) (Embed (Var x)))
print $ rebound
let substed = subst x (Var y) rebound
print $ substed
print $ unrebind substed
print $ rebindPass substed
Which outputs:
<<Var y>> {Var x}
<<Var y>> {Var y}
(Var y,{Var y})
<<Var y>> {Var 0 at 0}
If the equation holds true then the second and fourth lines should be
identical but they are not. Can someone explain why this is the
correct behavior or if the implementation is incorrect?
More information about the Haskell-Cafe
mailing list