| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Binrep.Type.Byte
Description
Safe, if silly, byte representation for use at the type level.
Word8 is a special type that GHC doesn't (and I think can't) promote to the
type level. We only have Naturals, which are unbounded. So we define a safe,
promotable representation, to allow us to prove well-sizedness at compile time.
Then we provide a bunch of type families and reifying typeclasses to enable
going between "similar" kinds (Natural) and types (Word8, ByteString)
respectively.
Type-level functionality is stored in TypeLevel because the
definitions are even sillier than the ones here.
Do not use this on the term level. That would be _extremely_ silly.
Synopsis
- class ByteVal (n :: Natural) where
- type family Length (a :: [k]) :: Natural where ...
- class ReifyBytes (ns :: [Natural]) where
- class WriteReifiedBytes (ns :: [Natural]) where
- writeReifiedBytes :: Addr# -> IO ()
Documentation
class ByteVal (n :: Natural) where Source #
Instances
class ReifyBytes (ns :: [Natural]) where Source #
Efficiently reify a list of type-level Natural bytes to to a bytestring
builder.
Attempting to reify a Natural larger than 255 results in a type error.
This is about as far as one should go for pointless performance here, I should think.
Methods
reifyBytes :: Builder Source #
Instances
| (n ~ Length ns, KnownNat n, WriteReifiedBytes ns) => ReifyBytes ns Source # | |
Defined in Binrep.Type.Byte Methods reifyBytes :: Builder Source # | |
class WriteReifiedBytes (ns :: [Natural]) where Source #
Methods
writeReifiedBytes :: Addr# -> IO () Source #
Instances
| WriteReifiedBytes ('[] :: [Natural]) Source # | |
Defined in Binrep.Type.Byte Methods writeReifiedBytes :: Addr# -> IO () Source # | |
| (ByteVal n, WriteReifiedBytes ns) => WriteReifiedBytes (n ': ns) Source # | |
Defined in Binrep.Type.Byte Methods writeReifiedBytes :: Addr# -> IO () Source # | |