Unsafe names for contexts, peeking under binders

[jonsterling]

There's a pattern here where I extend a context, peek under a scope, and then rebind the variable, like this:

welp <- extendCtx "x" s $ something (e // V "x")
return $ ("x" \\ welp)

This seems very unsafe, and is causing variables to get renamed which should not. For instance I can check λ[f] λ[x] f ∈ Π[a:Π[a:𝟚] 𝟚] Π[b:𝟚], which is clearly wrong.

I suspect the solution lies in not peeking under the binder like this using substitution & abstraction, but rather somehow getting it so that I can use fromScope and toScope. I just don't know how to do that here...

Thanks to notdan on #nothaskell for noticing this problem.

[co-dan]

One possible solution that I've found (which I am not entirely happy with, tbh) is using Bound.Name to keep track of the original names. The upside of this is that you can reuse the existing names for stuff like error reporting or whatnot, while simultaneously taking advantage of faster variable manipulation and unification.

Firstly, my expression datatype looks like this:

data Expr a = Var a
             | Lam Ty (Scope (Name String ()) Expr a)
             | Expr a :@: Expr a
    deriving (Foldable, Functor, Traversable, Show, Ord, Eq)

(I have a different representation for my lambda-calculus, I require every lambda variable to have an explicit type)

Then, the lambdas can be constructed like this:

lam :: String -> Ty -> Expr String -> Expr String
lam v t b = Lam t (abstract1Name v b)

Then, the type inference looks like this:

inferType (Lam t e) ctx = 
  let (n',ctx') = case bindings e of
                    (b:_) -> (name b, extendCtx (name b) t Nothing ctx)
                    [] -> ("dummy", ctx)
      t' = inferType (instantiate1 (Var n') e) ctx'
  in Arrow t t'

Here, we assume that the lambda binds at most one variable (which should be alright, if we are using smart constructor lam). If the lambda does not really bind a variable (i.e. the term lam[x].lam[y].x), then instantiate1 should have no effect, and the context should remain the same.

Things that I don't like about this approach:

• Is this approach actually sound? I think so, I dunno.
• This case analysis on bindings looks quite ad-hoc. Apparently, it does a fold every time we need to look at the bindings. Is the performance going to be OK?
• The String part of the name is hard-coded into the datatype.

[jonsterling]

Dan,

Thanks for investigating! I may ask Ed if he's got any suggestions here as well.

Best, Jon

On Jul 26, 2014, at 12:35 PM, Dan notifications@github.com wrote:

One possible solution that I've found (which I am not entirely happy with, tbh) is using Bound.Name to keep track of the original names. The upside of this is that you can reuse the existing names for stuff like error reporting or whatnot, while simultaneously taking advantage of faster variable manipulation and unification.

Firstly, my expression datatype looks like this:

data Expr a = Var a | Lam Ty (Scope (Name String ()) Expr a) | Expr a :@: Expr a deriving (Foldable, Functor, Traversable, Show, Ord, Eq) (I have a different representation for my lambda-calculus, I require every lambda variable to have an explicit type)

Then, the lambdas can be constructed like this:

lam :: String -> Ty -> Expr String -> Expr String lam v t b = Lam t (abstract1Name v b) Then, the type inference looks like this:

inferType (Lam t e) ctx = let (n',ctx') = case bindings e of (b:_) -> (name b, extendCtx (name b) t Nothing ctx) [] -> ("dummy", ctx) t' = inferType (instantiate1 (Var n') e) ctx' in Arrow t t' Here, we assume that the lambda binds at most one variable (which should be alright, if we are using smart constructor lam). If the lambda does not really bind a variable (i.e. the term lam[x].lam[y].x), then instantiate1 should have no effect, and the context should remain the same.

Things that I don't like about this approach:

Is this approach actually sound? I think so, I dunno. This case analysis on bindings looks quite ad-hoc. Apparently, it does a fold every time we need to look at the bindings. Is the performance going to be OK? The String part of the name is hard-coded into the datatype. — Reply to this email directly or view it on GitHub.