Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Various kinds of arrays (lists, vectors, bytestrings) with statically aserted length constraints encoded in their type.
Synopsis
- class KnownNat (n :: Nat)
- class KnownOrdering (o :: Ordering)
- newtype OpaqueString = OpaqueString {}
- opaqueLengthArray :: LengthArray o n ByteString -> LengthArray o n OpaqueString
- unOpaqueLengthArray :: LengthArray o n OpaqueString -> LengthArray o n ByteString
- data LengthArray (o :: Ordering) (n :: Nat) a
- type FixedLengthArray n a = LengthArray 'EQ n a
- fixedLengthArrayLength :: KnownNat n => LengthArray 'EQ n a -> Int
- type BoundedLengthArray n a = LengthArray 'LT (n + 1) a
- boundedLengthArrayBound :: KnownNat n => LengthArray 'LT n a -> Int
- unLengthArray :: LengthArray o n a -> a
- unsafeLengthArray :: a -> LengthArray o n a
- lengthArray :: forall o n a. (KnownOrdering o, KnownNat n, HasLength a) => a -> Maybe (LengthArray o n a)
- lengthArray' :: forall o n a. (KnownOrdering o, KnownNat n, HasLength a) => a -> LengthArray o n a
- boundLengthArray :: (KnownNat n, Array a) => a -> LengthArray 'LT n a
- boundLengthArrayFromList :: (KnownNat n, Array a) => [Elem a] -> LengthArray 'LT n a
- padLengthArray :: (KnownNat n, Array a) => a -> Elem a -> LengthArray 'EQ n a
- constLengthArray :: (KnownNat n, Array a) => Elem a -> LengthArray 'EQ n a
- emptyFixedLengthArray :: Array a => LengthArray 'EQ 0 a
- emptyBoundedLengthArray :: (CmpNat 0 n ~ 'LT, Array a) => LengthArray 'LT n a
- expandBoundedLengthArray :: CmpNat n m ~ 'LT => LengthArray 'LT n a -> LengthArray 'LT m a
- boundFixedLengthArray :: CmpNat n m ~ 'LT => LengthArray 'EQ n a -> LengthArray 'LT m a
- appendLengthArray :: Monoid a => LengthArray o n a -> LengthArray o m a -> LengthArray o (n + m) a
- fromLengthList :: Array a => LengthArray o n [Elem a] -> LengthArray o n a
Documentation
This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.
Since: base-4.7.0.0
natSing
class KnownOrdering (o :: Ordering) Source #
orderingVal
Instances
KnownOrdering 'EQ Source # | |
Defined in Network.ONCRPC.XDR.Array orderingVal :: proxy 'EQ -> Ordering | |
KnownOrdering 'GT Source # | |
Defined in Network.ONCRPC.XDR.Array orderingVal :: proxy 'GT -> Ordering | |
KnownOrdering 'LT Source # | |
Defined in Network.ONCRPC.XDR.Array orderingVal :: proxy 'LT -> Ordering |
newtype OpaqueString Source #
Instances
opaqueLengthArray :: LengthArray o n ByteString -> LengthArray o n OpaqueString Source #
unOpaqueLengthArray :: LengthArray o n OpaqueString -> LengthArray o n ByteString Source #
data LengthArray (o :: Ordering) (n :: Nat) a Source #
Assertion that the contained array satisfies compareLength
a n = o
Instances
type FixedLengthArray n a = LengthArray 'EQ n a Source #
Assertion that the contained array is exactly a static length
fixedLengthArrayLength :: KnownNat n => LengthArray 'EQ n a -> Int Source #
Static length of a FixedLengthArray
type BoundedLengthArray n a = LengthArray 'LT (n + 1) a Source #
Assertion that the contained array is at most a static length (inclusive)
boundedLengthArrayBound :: KnownNat n => LengthArray 'LT n a -> Int Source #
Static upper-bound (inclusive) of a BoundedLengthArray
unLengthArray :: LengthArray o n a -> a Source #
unsafeLengthArray :: a -> LengthArray o n a Source #
Unsafely create a LengthArray
without checking the length bound assertion.
May cause unpredictable behavior if the bound does not hold.
lengthArray :: forall o n a. (KnownOrdering o, KnownNat n, HasLength a) => a -> Maybe (LengthArray o n a) Source #
Safely create a LengthArray
out of an array if it conforms to the static length assertion.
lengthArray' :: forall o n a. (KnownOrdering o, KnownNat n, HasLength a) => a -> LengthArray o n a Source #
Create a LengthArray
or runtime error if the assertion fails: fromMaybe undefined .
lengthArray
boundLengthArray :: (KnownNat n, Array a) => a -> LengthArray 'LT n a Source #
Create a BoundedLengthArray
by trimming the given array if necessary.
boundLengthArrayFromList :: (KnownNat n, Array a) => [Elem a] -> LengthArray 'LT n a Source #
Create a BoundedLengthArray
by trimming the given array if necessary.
padLengthArray :: (KnownNat n, Array a) => a -> Elem a -> LengthArray 'EQ n a Source #
Create a FixedLengthArray
by trimming or padding (on the right) as necessary.
constLengthArray :: (KnownNat n, Array a) => Elem a -> LengthArray 'EQ n a Source #
Create a FixedLengthArray
filled with the same value.
emptyFixedLengthArray :: Array a => LengthArray 'EQ 0 a Source #
An empty FixedLengthArray
.
emptyBoundedLengthArray :: (CmpNat 0 n ~ 'LT, Array a) => LengthArray 'LT n a Source #
An empty BoundedLengthArray
.
expandBoundedLengthArray :: CmpNat n m ~ 'LT => LengthArray 'LT n a -> LengthArray 'LT m a Source #
Grow the bound of a BoundedLengthArray
.
boundFixedLengthArray :: CmpNat n m ~ 'LT => LengthArray 'EQ n a -> LengthArray 'LT m a Source #
Convert a FixedLengthArray
to a BoundedLengthArray
.
appendLengthArray :: Monoid a => LengthArray o n a -> LengthArray o m a -> LengthArray o (n + m) a Source #
Append to two LengthArray
s.
fromLengthList :: Array a => LengthArray o n [Elem a] -> LengthArray o n a Source #