lollipop
lollipop copied to clipboard
m0ar
Evaluation of ELam does not return correct environment
Eval of a ELam now returns a VFun and an environment where var is incorrectly unbound, but should return the environment produced by the inner eval produced inside the VFun
Why does eval return an environment at all? I don't think it should. Has it always done that?
Returning the environment with the variable bound would be a bad idea, since for instance the case for EApp uses the new environement. It would mean that the variable escapes it's scope...
We decided to introduce the environment in the eval-function to keep track of variables in a way which allows us to remove linear variables from the environment as they are used.
I see. I doubt that is a good strategy though. At least not the way it is implemented now because it introduces an evaluation order, destroying laziness. I'm guessing things like let x = undefined in 1 will now be undefined? (Or it would be if undefined worked propertly, maybe a better example would be using infinite lists)
That is true. Do you have any suggestion of how we would go about removing variables from the environment when they have been evaluated?
Maybe you can somehow avoid adding it to the environment in the first place? This depends a lot on how you represent linear expressions. Is there a special lambda abstraction for linear types? A special kind of function application?
Some possible ideas:
- Keep a separate environment of linear variables, in each function application split it into those that are used in the left branch and those that are used in the right. This needs to be done very efficiently if there is going to be any use.
- Keep an environment of references instead, and when the variable is used you change the reference (to point to error "reused linear variable" or such). This allows the value to be deallocated but maybe not the pointer to it.
- Have a more general solution for handling explicit memory management, where you can annotate the source tree with "remove this variable from the environment" e.g. add an ERelease Var Exp constructor to Exp. This could also be used for things like tail recursion although I'm not sure how efficient it is. Then you would need to have a separate pass or part of the type checker that adds these where appropriate for linear variables (always add them to one branch of every application for instance).
We removed the handling of linear types from the interpreter and eval-function and expand it in the type checker, since it's actually a type-feature.
The idea of modifying the environment to change the references of linear variables to point to an error is in line of how we wanted to do it in the first place, but we're not really sure of where this should be done, if not in the eval-function.
If you have a map that maps linear variables to references (M.Map Var (IORef Value) or such), when a linear variable is used you would use unsafePerformIO to fetch it's value and write undefined to it. Since this can only happen once per variable there is no risk in using unsafePerformIO or that the undefined value is inspected (if the program is type correct).
With a more clever representation it might even be possible to remove the variable completely including the reference.