Eric Dobson | 14 Apr 19:57 2013
Picon

Unbound: rebind and unrebind

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:

{-# 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"
(Continue reading)

Brent Yorgey | 22 Apr 22:18 2013

Re: Unbound: rebind and unrebind

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,
(Continue reading)

Eric Dobson | 23 Apr 07:44 2013
Picon

Re: Unbound: rebind and unrebind

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.
(Continue reading)


Gmane