Conversation

Notices

1. Embed this notice
   julesh (julesh@mathstodon.xyz)'s status on Monday, 25-Nov-2024 00:00:25 JST julesh

   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

   • Embed this notice
     julesh (julesh@mathstodon.xyz)'s status on Monday, 25-Nov-2024 00:00:36 JST julesh

     in reply to

     I think this can be extended from affine to linear theories, now you need to take more seriously that this thing is bidirectional, by which I mean "yet another thing that's secretly a dependent affine traversal". When you pass through a lambda you add its variable(s) to your context, but then when you've finished checking the lambda's subterm you pass backwards up through the lambda again, at which point the lambda checks that all the variables it added are no longer there, and fails with a quantity error if any are

   • Embed this notice
     TobyBartels (tobybartels@mathstodon.xyz)'s status on Monday, 25-Nov-2024 01:19:35 JST TobyBartels

     in reply to

     @julesh : I know I wasn't part of the original conversation, but that all sounds correct to me.

     Since the question about quantity is, as with a scope error, whether it's 0 or not, I'd still think of this quantity error as more like a scope error, just in reverse. In a regular scope error, x is supposed to be in scope but it's not; in this reverse scope error, x isn't supposed to be in scope but it is.