Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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 Natural
s, 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.
reifyBytes :: Builder Source #
Instances
(n ~ Length ns, KnownNat n, WriteReifiedBytes ns) => ReifyBytes ns Source # | |
Defined in Binrep.Type.Byte reifyBytes :: Builder Source # |
class WriteReifiedBytes (ns :: [Natural]) where Source #
writeReifiedBytes :: Addr# -> IO () Source #
Instances
WriteReifiedBytes ('[] :: [Natural]) Source # | |
Defined in Binrep.Type.Byte writeReifiedBytes :: Addr# -> IO () Source # | |
(ByteVal n, WriteReifiedBytes ns) => WriteReifiedBytes (n ': ns) Source # | |
Defined in Binrep.Type.Byte writeReifiedBytes :: Addr# -> IO () Source # |