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

2013-04-22 Thread 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-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

2013-04-22 Thread Eric Dobson
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