kowainik/membrain

🧠 Type-safe memory units

membrain

"People think dreams aren't real just because they aren't made of matter, of particles. Dreams are real. But they are made of viewpoints, of images, of memories and puns and lost hopes."

― Neil Gaiman

This package implements type-safe memory units. It pursues the following goals:

1. Focus on correctness.
2. Low amount of boilerplate should be required to use the library.

The ideas behind this package are described in the following blog post:

• Insane in the Membrain

The library is built around the following data type:

newtype Memory (mem :: Nat) = Memory
    { unMemory :: Natural
    }

This data type stores every memory internally as bits. However, unit multiplier is stored as type-level natural number. This approach allows to represent different units and implement instances for them with low amount of boilerplate.

membrain implements various useful functions to work with Memory:

1. Smart constructors.
2. Conversion functions.
3. Pretty displaying.
4. Dependently-typed parsing.
5. Numeric functions.
6. Type-safe wrappers around functions from base.

Acknowledgement

Icons made by Kiranshastry from Flaticon is licensed by CC 3.0 BY.

membrain's Issues

Implement property-based roundtrip tests for showMemory/readMemory

Smart Read instance

Update default branch to main

Derive Show, move current implementation to separate function

Implement conversion functions from Memory type

Use Proxy#

Improve documentation

• Show uses cases in the README
• Better cabal description
• Check the whole Haddock and try to improve it

Pretty Show instance

Implement property-based tests for conversion functions

Implement numeric functions to work with Memory type

Implement type-level testing

Bounded Memory

Recently I was optimizing some code that was using regexes to search DNA strings:

agggtaaa|tttaccct
[cgt]gggtaaa|tttaccc[acg]
a[act]ggtaaa|tttacc[agt]t
ag[act]gtaaa|tttac[agt]ct
agg[act]taaa|ttta[agt]cct
aggg[acg]aaa|ttt[cgt]ccct
agggt[cgt]aa|tt[acg]accct
agggta[cgt]a|t[acg]taccct
agggtaa[cgt]|[acg]ttaccct

Conveniently, all of these are of length 8 and there are only 4 possible letters, so I can fit one of these in a Word16:

-- Holds 8 DNA letters, each letter is 2 bits
type Buffer = Word16

And I can push a new letter to the front of my buffer and simultaneously remove the last like so:

type DNALetter = Buffer
push :: DNALetter -> Buffer -> Buffer
push l b = shiftL b 2 .|. l

Searching then, is done by pushing one letter at a time and checking if the buffer matches any of the strings from the regexes.

It would be nice if the type of DNALetter reflected that a letter should be 2 bits long, which I can express with Membrain like so:

type DNALetter = Memory (Bit * 2)
push :: DNALetter -> Buffer -> Buffer
push l b = shiftL b 2 .|. fromIntegral (unMemory l)

Now, I have 2 issues with this:

1. I believe this would make my code significantly slower because now I have to cast the letter to a Word16 from a Natural
2. It makes it possible to push more letters than my buffer can actually fit

---

I propose adding a bounded memory type

newtype BoundedMemory (unit :: Nat) (max :: Nat) where
  { unMemory :: WordByBits (unit * max) }

Here, unit would be the same as mem in Memory, max would be the how many units we can hold at most, and WordByBits would be the smallest word big enough to store max units.

One possible implementation of WordByBits:

import GHC.TypeLits
import Data.Word
import Numeric.Natural

type family Log2W (n :: Nat) :: * where
  Log2W 0 = Word8
  Log2W 1 = Word16
  Log2W 2 = Word32
  Log2W 3 = Word32
  Log2W 4 = Word64
  Log2W 5 = Word64
  Log2W 6 = Word64
  Log2W 7 = Word64
  Log2W _ = Natural

type WordByBits n = Log2W (Div n 8)     -- Word by number of bits
type StingyWord n = WordByBits (Log2 n) -- Word by cardinality

Usage example:

type Letter = 2 * Bit
type Buffer = BoundedMemory Letter 8 -- Word16, yay!

push l b = shiftL b 2 .|. unMemory b -- No cast, I can even coerse!

Implement more memory-safe functions from 'base'

Implement unit testing for constructors/functions

Add `-Wmissing-deriving-strategies` to cabal ghc options

Also, add DerivingStrategies to the list of default extensions.

Introduce 'doctest' tests

Introduce type aliases and smart constructors

Introduce Memory type

Use Proxy# instead of Proxy

This is better for performance and memory usage. We have two places where we can improve things:

• For naturals:

  • membrain/src/Membrain/Memory.hs

    Lines 320 to 321 in 3b649d7

    	nat :: forall (mem :: Nat) . KnownNat mem => Natural
    	nat = natVal (Proxy @mem)

• For symbols

  • membrain/src/Membrain/Units.hs

    Lines 139 to 140 in 5c23036

    	unitSymbol :: forall (mem :: Nat) . KnownUnitSymbol mem => String
    	unitSymbol = symbolVal $ Proxy @(UnitSymbol mem)

Support GHC-8.8

Allow doctest-0.17

commercialhaskell/stackage#5406

Add compile-time check for terminating decimal

See this comment:

membrain/src/Membrain/Memory.hs

Line 52 in 0ed5b57

TODO: check this statically

Support 8.10

Implement Semigroup and Monoid instances for Memory

Additionally, implement property tests for Semigroup/Monoid laws