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
