Embed Notice

QRT https://mathstodon.xyz/@zanzi/113538216107803309
Ok so I was thinking about this yesterday. For scope checking in an affine type system I think there's a fairly obvious looking trick, where you traverse the term while mutating a context as you go. Each Var rule will check that its name exists in the context, if it is not then fail, and if it is then remove it from the scope before passing it to the next thing in the traversal. For example, checking lambda x. Pair (Var x) (Var x) in the empty context, you will go under the lambda and check Pair (Var x) (Var x) in the context [x], then go to the first Var x in the context [x], which succeeds and sends the empty context to the second Var x, which then fails because x is not in scope. So there are no explicit quantity errors, they become scope errors