sext-0.1.0.0: Lists, Texts and ByteStrings with type-encoded length

Safe HaskellNone
LanguageHaskell2010

Data.Sext

Contents

Description

Sext (static text) provides type-level safety for basic operations on string-like types (finite lists of elements). Use it when you need static guarantee on lengths of strings produced in your code.

An example application would be a network exchange protocol built of packets with fixed-width fields:

mkPacket :: String -> Sext 32 String
mkPacket inp =
  -- 5-character version signature
  $(sext "PKT10") `append`
  -- 25-character payload
  payload `append`
  -- 2-character payload checksum
  checksum
  where
    payload = createLeft ' ' inp
    checksum :: Sext 2 String
    checksum = createLeft ' ' $
               show $ length payload `mod` 100

message :: Sext 64 String
message = mkPacket "Hello" `append` mkPacket "world"

Sext combinators are defined for members of Sextable class. The package includes Sextable instances for several common types.

This module is meant to be imported qualifed, e.g.

import qualified Data.Sext as S

Synopsis

Constructing Sexts

See also unsafeCreate

createLeft :: forall a i. (Sextable a, KnownNat i) => Elem a -> a -> Sext i a Source

Safely create a Sext, possibly altering the source to match target length. If target length is less than that of the source, the source gets truncated. If target length is greater, the source is padded using the provided basic element. Elements on the left are preferred.

>>> createLeft ' ' "foobarbaz" :: Sext 6 String
"foobar"
>>> createLeft '#' "foobarbaz" :: Sext 12 String
"foobarbaz###"

createRight :: forall a i. (Sextable a, KnownNat i) => Elem a -> a -> Sext i a Source

Just like createLeft, except that elements on the right are preferred.

>>> createRight '@' "foobarbaz" :: Sext 6 String
"barbaz"
>>> createRight '!' "foobarbaz" :: Sext 12 String
"!!!foobarbaz"

sext :: LitS -> Q Exp Source

Type-safe Sext constructor macro for string literals.

Example:

$(sext "Foobar")

compiles to

unsafeCreate "Foobar" :: forall a. (IsString a, Sextable a) => Sext 6 a

where 6 is the string length obtained at compile time.

create :: forall a i. (Sextable a, KnownNat i) => a -> Maybe (Sext i a) Source

Attempt to safely create a Sext if it matches target length.

>>> create "foobar" :: Maybe (Sext 6 String)
Just "foobar"
>>> create "barbaz" :: Maybe (Sext 8 String)
Nothing

This is safer than unsafeCreate and unlike with createLeft / createRight the source value is left unchanged. However, this implies a further run-time check for Nothing values.

replicate :: forall a i. (Sextable a, KnownNat i) => Elem a -> Sext i a Source

Construct a new Sext from a basic element.

>>> replicate '=' :: Sext 10 String
"=========="

Working with Sexts

append :: forall a m n. Sextable a => Sext m a -> Sext n a -> Sext (m + n) a Source

Append two Sexts together.

>>> append "foo" "bar" :: Sext 6 String
"foobar"

take :: forall a m n. (Sextable a, KnownNat m, KnownNat n, n <= m) => Sext m a -> Sext n a Source

Reduce Sext length, preferring elements on the left.

>>> take "Foobar" :: Sext 3 String
"Foo"

drop :: forall a m n. (Sextable a, KnownNat m, KnownNat n, n <= m) => Sext m a -> Sext n a Source

Reduce Sext length, preferring elements on the right.

>>> drop "Foobar" :: Sext 2 String
"ar"

map :: Sextable a => (Elem a -> Elem a) -> Sext m a -> Sext m a Source

padLeft :: forall a m n. (Sextable a, KnownNat m, KnownNat (n - m), n ~ ((n - m) + m), m <= n) => Elem a -> Sext m a -> Sext n a Source

Fill a Sext with extra elements up to target length, padding original elements to the left.

padRight :: forall a m n. (Sextable a, KnownNat m, KnownNat (n - m), n ~ (m + (n - m)), m <= n) => Elem a -> Sext m a -> Sext n a Source

Like padLeft, but original elements are padded to the right.

length :: forall a m. KnownNat m => Sext m a -> Int Source

Obtain value-level length.

Sextable class

class Sextable a where Source

Class of types which can be assigned a type-level length.

Minimal complete definition

unsafeCreate, unwrap, length, append, replicate, map, take, drop

Methods

unsafeCreate :: a -> Sext i a Source

Simply wrap a value in a Sext as is, assuming any length.

For example, an expression like

unsafeCreate "somestring" :: Sext 50 String

will typecheck, although the stored length information will not match actual string size. This may result in wrong behaviour of all functions defined for Sext.

Use it only when you know what you're doing.

When implementing new Sextable instances, code this to simply apply the constructor of Sext.

unwrap :: Sext i a -> a Source

Forget type-level length, obtaining the underlying value.

Instances