Consider replacing FrameInstr with a function
Clarification and motivation
We have FrameInstr
constructor in the typed morley Instr
, which essentially takes an Instr
operating on a truncated stack and generalizes it to operate on a non-truncated stack.
We used a separate constructor due to some challenges in convincing GHC this is sound, however it would be beneficial to replace this with a function without adding new constructors:
- it would slightly simplify the interpreter code
- it would improve interpreter performance, especially in the case of nested frames
- it would allow our optimizer to optimize across
framed
blocks
Acceptance criteria
-
FrameInstr
constructor is removed -
frameInstr :: Instr a b -> Instr (a ++ s) (b ++ s)
(possibly constrained) is added
Edited by Nikolay Yakimov