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...
On Mon, Apr 22, 2013 at 1:18 PM, Brent Yorgey
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...
[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