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.

Documentation

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

withSomeSymbol :: SomeSymbol -> (forall x. KnownSymbol x => Proxy x -> r) -> r

Convenience combinator missing in TypeLits, See Examples.TypedEncoding.SomeEnc.SomeAnnotation "Examples.TypedEncoding.SomeEnc.someAnnValue"

Since: 0.2.0.0

proxyCons :: forall (x :: Symbol) (xs :: [Symbol]). Proxy x -> Proxy xs -> Proxy (x ': xs)

(Moved from previously defined module Data.TypedEncoding.Common.Types.SomeAnnotation)

Since: 0.2.0.0

type family Append (xs :: [k]) (ys :: [k]) :: [k] where ...

Type level list append

(moved from Data.TypedEncoding.Common.Class.Common)

Since: 0.1.0.0

Equations

Append '[] xs = xs

Append (y ': ys) xs = y ': Append ys xs

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

Since: 0.2.1.0

Equations

AcceptEq _ EQ = True

AcceptEq msg _ = TypeError msg

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

Since: 0.4.0.0

Equations

OrdBool EQ = True

OrdBool _ = False

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

Since: 0.2.1.0

Equations

And True True = True

And _ _ = False

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

Since: 0.2.1.0

Equations

Or False False = False

Or _ _ = True

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

Since: 0.2.1.0

Equations

If True a _ = a

If False _ b = b

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

Since: 0.2.1.0

Equations

Repeat 0 s = ""

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

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

Since: 0.2.1.0

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