[Haskell-cafe] Unbound: rebind and unrebind

[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 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?
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe