[Haskell-cafe] Unbound: rebind and unrebind

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