Skip to content

Instantly share code, notes, and snippets.

@txus
Last active July 30, 2018 20:54
Show Gist options
  • Save txus/a0583645f0aa11f75f28 to your computer and use it in GitHub Desktop.
Save txus/a0583645f0aa11f75f28 to your computer and use it in GitHub Desktop.
Memory as a dependently-typed effect (scroll down for examples!)

Memory as an effect

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!!!!!!

module Memory
import Effects
data Allocated : Nat -> Nat -> Type where
MkAllocated : (allocated : Nat) -> (available : Nat) -> Allocated allocated available
allocateMemory : (m : Nat) -> (n : Nat) -> (smaller: LTE m n) -> IO ()
allocateMemory wanted available _ = pure ()
freeMemory : (m : Nat) -> (n : Nat) -> (smaller: LTE m n) -> IO ()
freeMemory bytes allocated _ = pure ()
data Memory : Effect where
Allocate : (n : Nat) ->
(smaller: LTE n m) ->
sig Memory () (Allocated a m) (\_ => (Allocated (a + n) (m - n)))
Free : (n : Nat) ->
(smaller: LTE n a) ->
sig Memory () (Allocated a m) (\_ => (Allocated (a - n) (m + n)))
Handler Memory IO where
handle (MkAllocated allocated available) (Allocate wanted lte) k = do allocateMemory wanted available lte
k () (MkAllocated (allocated + wanted) (available - wanted))
handle (MkAllocated allocated available) (Free toFree lte) k = do freeMemory toFree allocated lte
k () (MkAllocated (allocated - toFree) (available + toFree))
MEMORY : Type -> EFFECT
MEMORY a = MkEff a Memory
-- Some convenience functions
allocate : (n : Nat) -> {default (%runElab (search' 100000 [])) smaller : LTE n m} -> Eff () [MEMORY (Allocated a m)]
[MEMORY (Allocated (a + n) (m - n))]
allocate bytes {smaller} = call (Allocate bytes smaller)
free : (n : Nat) -> {default (%runElab (search' 100000 [])) smaller : LTE n a} -> Eff () [MEMORY (Allocated a m)]
[MEMORY (Allocated (a - n) (m + n))]
free bytes {smaller} = call (Free bytes smaller)
-- Some type aliases for effectful memory programs
||| The type of a memory program which leaves its initial allocated and
||| available memory untouched, namely that it doesn't leak memory.
NonLeaky : (allocated : Nat) -> (available : Nat) -> Type
NonLeaky alloc avail = Eff () [MEMORY (Allocated alloc avail)]
[MEMORY (Allocated alloc avail)]
infixr 6 |->|
||| The type of a memory program that starts off with some allocated and
||| available memory and ends up with different allocated and available memory.
(|->|) : (Nat, Nat) -> (Nat, Nat) -> Type
(alloc1, avail1) |->| (alloc2, avail2) = Eff () [MEMORY (Allocated alloc1 avail1)]
[MEMORY (Allocated alloc2 avail2)]
-- Examples
-- 0 bytes allocated so far, 16 bytes available
nonLeaky : NonLeaky 0 16
nonLeaky = do allocate 4
allocate 8
free 12
-- Starting off with 0 bytes allocated and 16 bytes available,
-- and ending with 4 bytes allocated and thus 12 available
allocatesFourBytes : (0, 16) |->| (4, 12)
allocatesFourBytes = do allocate 4
-- Local Variables:
-- idris-load-packages: ("effects")
-- End:
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment