### Re: [Haskell-cafe] Unbound: rebind and unrebind

Hi Eric, On Sun, Apr 14, 2013 at 10:57:43AM -0700, Eric Dobson wrote: 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: You're right that you *can* write a program involving a Rebind without a higher level Bind. But you *should not*. This is explained in the documentation [1] and in the paper [2]. Briefly, there are two classes of types, term types and pattern types. You should only use term types to represent data in your programs. Rebind constructs a pattern type, and as such should only be used in the context of an enclosing Bind. It would be much nicer if we were able to track this distinction directly in Haskell's type system and somehow prevent users from using pattern types directly, but we do not know of a way to do this. -Brent [1] http://hackage.haskell.org/packages/archive/unbound/0.4.1.1/doc/html/Unbound-LocallyNameless.html#g:4 [2] Stephanie Weirich, Brent A. Yorgey, and Tim Sheard. Binders Unbound. ICFP'11, September 2011, Tokyo, Japan. http://www.cis.upenn.edu/~byorgey/papers/binders-unbound.pdf. {-# 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@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? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

### Re: [Haskell-cafe] Unbound: rebind and unrebind

Where I am making the type error (that cannot be caught)? I would assume it would be the 'let substed = subst x (Var y) rebound', line in particular the third argument. But the documentation of subst does not use either t or p in its type signature, so the rule doesn't seem to apply [1]. And I would expect to be able to substitute into patterns in addition to terms, so that it could enter embeded terms. http://hackage.haskell.org/packages/archive/unbound/0.4.1.1/doc/html/Unbound-LocallyNameless.html#v:subst On Mon, Apr 22, 2013 at 1:18 PM, Brent Yorgey byor...@seas.upenn.edu wrote: Hi Eric, On Sun, Apr 14, 2013 at 10:57:43AM -0700, Eric Dobson wrote: 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: You're right that you *can* write a program involving a Rebind without a higher level Bind. But you *should not*. This is explained in the documentation [1] and in the paper [2]. Briefly, there are two classes of types, term types and pattern types. You should only use term types to represent data in your programs. Rebind constructs a pattern type, and as such should only be used in the context of an enclosing Bind. It would be much nicer if we were able to track this distinction directly in Haskell's type system and somehow prevent users from using pattern types directly, but we do not know of a way to do this. -Brent [1] http://hackage.haskell.org/packages/archive/unbound/0.4.1.1/doc/html/Unbound-LocallyNameless.html#g:4 [2] Stephanie Weirich, Brent A. Yorgey, and Tim Sheard. Binders Unbound. ICFP'11, September 2011, Tokyo, Japan. http://www.cis.upenn.edu/~byorgey/papers/binders-unbound.pdf. {-# 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@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? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe