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 doing) a simple approach to managing memory allocations and frees in the type system is outlined, together with some convenient sugar to make it nicer to use.
Scroll down to the examples section to see a couple of examples, namely:
-
nonLeaky
: a program that starts out with 0 bytes allocated and 16 available to its disposal, and ends up with the same as it frees all the memory that it allocated. -
allocatesFourBytes
: a program that starts out with 0 bytes allocated and 16 available, and ends up with 4 bytes allocated and 12 available.
Now, the cool thing is that if you try to change the numbers in allocate
and
free
calls, you'll get compile-time errors. All thanks to Idris and
dependent types! Yay!!!!!!