adding variables/types to a typing environment

Question

I have an environment which contains a set of tokens that I have already come across; when I look at a new token I want to add that token to the current environment. Basically I want to express a set-union operation on the environment that I perform parsing in.

something like Γ' = {Γ , x}

and if I want to delete the variable 'x' (remove x from the environment)

Γ' = Γ - x if x ∈ Γ .

What is the proper way to write these two formalisms. Thanks.

Answer 1

Basically you want to implement your environment as some data structure that supports insert, delete and search, and pass that data structure to your parser. I imagine in your parser, you would look at the current token, does the appropriate update to the environment, then recursively call the parser on the next token then pass in the updated environment.

Which particular data structure to use is up to you, binary search tree or its variants would do fine, or you can just use Haskell's built-in list type if you don't care about performance.

EDIT: To write down this process formally, you can borrow from type rules and how they are written, here is a reference. For example, we can denote that a program is successfully parsed by Γ ⊢ program:OK (I'm not sure if you want to deal with actual types here). Then, to add a token into the environment, you can write

    Γ,id ⊢ program:OK
-------------------------
  Γ ⊢ add id, program:OK

To remove a token, you can write

        Γ ⊢ program:OK
------------------------------
  Γ,id ⊢ remove id, program:OK