Data.TypedEncoding.Common.Util.TypeLits

TypeLits related utilities.

Lots of this could be avoided by adding singletons as dependency.

Uses symbols library for its ToList type family.

Currently this is spread out in different modules

• Data.TypedEncoding.Common.Class.Util
• Data.TypedEncoding.Common.Types.SomeAnnotation

(TODO) these will need to get consolidated.

Documentation

>>> :set -XScopedTypeVariables -XTypeFamilies -XKindSignatures -XDataKinds

type family AcceptEq (msg :: ErrorMessage) (c :: Ordering) :: Bool where ...

Equations

AcceptEq _ EQ = True

AcceptEq msg _ = TypeError msg

type family OrdBool (c :: Ordering) :: Bool where ...

Equations

OrdBool EQ = True

OrdBool _ = False

type family And (b1 :: Bool) (b2 :: Bool) :: Bool where ...

Equations

And True True = True

And _ _ = False

type family Or (b1 :: Bool) (b2 :: Bool) :: Bool where ...

Equations

Or False False = False

Or _ _ = True

type family If (b1 :: Bool) (a :: k) (b :: k) :: k where ...

Equations

If True a _ = a

If False _ b = b

type family Repeat (n :: Nat) (s :: Symbol) :: Symbol where ...

Equations

Repeat 0 s = ""

Repeat n s = AppendSymbol s (Repeat (n - 1) s)

type family Fst (s :: (k, h)) :: k where ...

Equations

Fst ((,) a _) = a

type family Dupl (s :: k) :: (k, k) where ...

Equations

Dupl a = (,) a a

type family Concat (s :: [Symbol]) :: Symbol where ...

>>> :kind! Concat (LDrop 6 (ToList "bool: \"r-ban:ff-ff\" | \"r-ban:ffff\""))
...
= "\"r-ban:ff-ff\" | \"r-ban:ffff\""

Since: 0.2.1.0

Equations

Concat '[] = ""

Concat (x ': xs) = AppendSymbol x (Concat xs)

type family Drop (n :: Nat) (s :: Symbol) :: Symbol where ...

Equations

Drop n s = Concat (LDrop n (ToList s))

type family LDrop (n :: Nat) (s :: [k]) :: [k] where ...

Since: 0.2.1.0

Equations

LDrop 0 s = s

LDrop n '[] = '[]

LDrop n (x ': xs) = LDrop (n - 1) xs

type family Take (n :: Nat) (s :: Symbol) :: Symbol where ...

>>> :kind! Take 3 "123456"
...
= "123"

Since: 0.2.1.0

Equations

Take n s = Concat (LTake n (ToList s))

type family LTake (n :: Nat) (s :: [k]) :: [k] where ...

Since: 0.2.1.0

Equations

LTake 0 s = '[]

LTake n '[] = '[]

LTake n (x ': xs) = x ': LTake (n - 1) xs

type family TakeUntil (s :: Symbol) (stop :: Symbol) :: Symbol where ...

Equations

TakeUntil s stop = Concat (LTakeUntil (ToList s) stop)

type family LTakeUntil (s :: [Symbol]) (stop :: Symbol) :: [Symbol] where ...

Since: 0.2.1.0

Equations

LTakeUntil '[] _ = '[]

LTakeUntil (x ': xs) stop = LTakeUntilHelper (x ': LTakeUntil xs stop) (CmpSymbol x stop)

type family LTakeUntilHelper (s :: [Symbol]) (o :: Ordering) :: [Symbol] where ...

Equations

LTakeUntilHelper '[] _ = '[]

LTakeUntilHelper (x ': xs) EQ = '[]

LTakeUntilHelper (x ': xs) _ = x ': xs

type family Length (s :: Symbol) :: Nat where ...

Since: 0.2.1.0

Equations

Length x = LLengh (ToList x)

type family LLengh (s :: [k]) :: Nat where ...

Since: 0.2.1.0

Equations

LLengh '[] = 0

LLengh (x ': xs) = 1 + LLengh xs

type family LLast (s :: [Symbol]) :: Symbol where ...

>>> :kind! LLast '["1","2","3"]
...
= "3"

Since: 0.2.2.0

Equations

LLast '[] = TypeError (Text "Empty Symbol list not allowed")

LLast '[x] = x

LLast (_ ': xs) = LLast xs

type family Snoc (s :: [k]) (t :: k) :: [k] where ...

>>> :kind! Concat (Snoc '["1","2","3"] "4")
...
= "1234"

Since: 0.2.2.0

Equations

Snoc '[] x = '[x]

Snoc (x ': xs) y = x ': Snoc xs y

type family UnSnoc (s :: [k]) :: ([k], k) where ...

:kind! UnSnoc '["1","2","3"] ... = '( (':) Symbol "1" ((':) Symbol "2" ('[] Symbol)), "3")

Since: 0.2.2.0

Equations

UnSnoc '[] = TypeError (Text "Empty list, no last element")

UnSnoc '[x] = (,) '[] x

UnSnoc (x ': xs) = UnSnocHelper x (UnSnoc xs)

type family UnSnocHelper (s :: k) (t :: ([k], k)) :: ([k], k) where ...

Equations

UnSnocHelper y ((,) xs x) = (,) (y ': xs) x