What if we treated memory as a side-effect?
Idris lets us track lots of things in the type system, in order to get errors at compile-time rather than at runtime. One of the tools that lets us do this in Idris is called Effects, and they're used to keep track of state, to manage file handlers, and lots more.
In barely 40 lines of Idris (which could be less if I had any idea what I'm