Safe Haskell	Safe
Language	Haskell2010

Data.TypedEncoding.Common.Util.TypeLits

Description

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

(TODO) these will need to get consolidated.

Synopsis

type family AcceptEq (msg :: ErrorMessage) (c :: Ordering) :: Bool where ...
type family And (b1 :: Bool) (b2 :: Bool) :: Bool where ...
type family Or (b1 :: Bool) (b2 :: Bool) :: Bool where ...
type family Repeat (n :: Nat) (s :: Symbol) :: Symbol where ...
type family Fst (s :: (k, h)) :: k where ...
type family Dupl (s :: k) :: (k, k) where ...
type family Concat (s :: [Symbol]) :: Symbol where ...
type family Drop (n :: Nat) (s :: Symbol) :: Symbol where ...
type family LDrop (n :: Nat) (s :: [k]) :: [k] where ...
type family Take (n :: Nat) (s :: Symbol) :: Symbol where ...
type family LTake (n :: Nat) (s :: [k]) :: [k] where ...
type family TakeUntil (s :: Symbol) (stop :: Symbol) :: Symbol where ...
type family LTakeUntil (s :: [Symbol]) (stop :: Symbol) :: [Symbol] where ...
type family LTakeUntilHelper (s :: [Symbol]) (o :: Ordering) :: [Symbol] where ...
type family Length (s :: Symbol) :: Nat where ...
type family LLengh (s :: [k]) :: Nat where ...
type family LLast (s :: [Symbol]) :: Symbol where ...
type family Snoc (s :: [k]) (t :: k) :: [k] where ...
type family UnSnoc (s :: [k]) :: ([k], k) where ...
type family UnSnocHelper (s :: k) (t :: ([k], k)) :: ([k], k) where ...

Documentation

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

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

Equations

AcceptEq _ EQ = True
AcceptEq msg _ = TypeError msg

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

Equations

And True True = True
And _ _ = False

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

Equations

Or False False = False
Or _ _ = True

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

Equations

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

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

Equations

Fst ((,) a _) = a

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

Equations

Dupl a = (,) a a

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

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

Equations

Concat '[] = ""
Concat (x ': xs) = AppendSymbol x (Concat xs)

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

Equations

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

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

:kind! LDrop 6 (ToList "bool: "r-ban:ff-ff" | "r-ban:ffff"")

Equations

LDrop 0 s = s
LDrop n '[] = '[]
LDrop n (x ': xs) = LDrop (n - 1) xs

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

:kind! Take 3 "123456"

Equations

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

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

:kind! LTake 3 (ToList "123456")

Equations

LTake 0 s = '[]
LTake n '[] = '[]
LTake n (x ': xs) = x ': LTake (n - 1) xs

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

Equations

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

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

Equations

LTakeUntil '[] _ = '[]
LTakeUntil (x ': xs) stop = LTakeUntilHelper (x ': LTakeUntil xs stop) (CmpSymbol x stop)

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

Equations

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

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

Equations

Length x = LLengh (ToList x)

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

Equations

LLengh '[] = 0
LLengh (x ': xs) = 1 + LLengh xs

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

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

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 ... Source #

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

Equations

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

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

:kind! UnSnoc '["1","2","3"]

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 ... Source #

Equations

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