L-as
commented
1 year ago If you have a term then interpret e.g. a linear variable to a free variable,
then you have a new term morally that is equivalent modulo that one point.
It shouldn't be feasible for any part of the term to depend on this being a linear variable.
Imagine you have a node that stores a Term (LinVar a : ls) tag and preserves the LinVar in the languages,
then interpreting this would result in a situation where this node is "opened up", then
the interpreters are applied to the subnodes, and we use the interpreters to transform the ls to
something we can understand, without interpreting LinVar into something else.
In practice, this means you can't interpret it, even though it looks like you can.
What other implications does this have?
Imagine you have a similar situation, but fix another language that isn't LinVar,
which you transform into a LinVar then use within a linear lambda.
This is well-typed, does it break soundness? I will think about it more.
Especially important in the context of #42 .