sext-0.1.3: Lists, Texts, ByteStrings and Vectors 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:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
import Data.Sext

mkPacket :: ByteString -> Sext 32 ByteString
mkPacket inp =
  -- 5-character version signature
  $(sext "PKT10") `append`
  -- 25-character payload
  payload `append`
  -- 2-character payload checksum
  checksum
  where
    payload = createLeft 0x20 inp
    checksum :: Sext 2 ByteString
    checksum = createLeft 0x20 $
               pack $ show $ Data.Sext.length payload `mod` 100

message :: Sext 64 ByteString
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 $(sext "foo") $(sext "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 $(sext "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 $(sext "Foobar") :: Sext 2 String
"ar"

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

Map a Sext to a Sext of the same length.

>>> map toUpper $(sext "Hello") :: Sext 5 String
"HELLO"

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

Associated Types

data Sext (i :: Nat) a Source #

Data family which wraps values of the underlying type giving them a type-level length. Sext 6 t means a value of type t of length 6.

type Elem a Source #

Basic element type. For Sextable [a], this is a.

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

Sextable ShortByteString Source #

Sextable instance for ShortByteString uses intermediate ByteStrings (pinned) for all modification operations.

Sextable ByteString Source # 
Sextable Text Source # 

Associated Types

data Sext (i :: Nat) Text :: * Source #

type Elem Text :: * Source #

Sextable [a] Source # 

Associated Types

data Sext (i :: Nat) [a] :: * Source #

type Elem [a] :: * Source #

Methods

unsafeCreate :: [a] -> Sext i [a] Source #

unwrap :: Sext i [a] -> [a] Source #

length :: [a] -> Int Source #

append :: [a] -> [a] -> [a] Source #

replicate :: Int -> Elem [a] -> [a] Source #

map :: (Elem [a] -> Elem [a]) -> [a] -> [a] Source #

take :: Int -> [a] -> [a] Source #

drop :: Int -> [a] -> [a] Source #

Sextable (Vector a) Source # 

Associated Types

data Sext (i :: Nat) (Vector a) :: * Source #

type Elem (Vector a) :: * Source #

Methods

unsafeCreate :: Vector a -> Sext i (Vector a) Source #

unwrap :: Sext i (Vector a) -> Vector a Source #

length :: Vector a -> Int Source #

append :: Vector a -> Vector a -> Vector a Source #

replicate :: Int -> Elem (Vector a) -> Vector a Source #

map :: (Elem (Vector a) -> Elem (Vector a)) -> Vector a -> Vector a Source #

take :: Int -> Vector a -> Vector a Source #

drop :: Int -> Vector a -> Vector a Source #