Data.Variant.Types

Documentation

natValue :: forall (n :: Nat) a. (KnownNat n, Num a) => a

Get a Nat value

natValue' :: forall (n :: Nat). KnownNat n => Word

Get a Nat value as a Word

type Index (n :: Nat) (l :: [k]) = Index' n l l

Indexed access into the list

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

Concat two type lists

Equations

Concat '[] '[] = '[]

Concat '[] ys = ys

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

type family Length (xs :: [k]) :: Nat where ...

Get list length

Equations

Length xs = Length' 0 xs

type family Product (xs :: [Type]) (ys :: [Type]) :: [Type] where ...

Product of two lists

Equations

Product '[] ys = '[]

Product xy '[] = '[]

Product (x : xs) ys = Concat (Product' x ys) (Product xs ys)

type family Remove (a :: k) (l :: [k]) :: [k] where ...

Remove a in l

Equations

Remove a '[] = '[]

Remove a (a ': as) = Remove a as

Remove a (b ': as) = b ': Remove a as

type family Nub (l :: [k]) :: [k] where ...

Keep only a single value of each type

Equations

Nub xs = Reverse (Nub' xs '[])

type family Reverse (l :: [k]) :: [k] where ...

Reverse a list

Equations

Reverse l = Reverse' l '[]

type IndexOf (x :: k) (xs :: [k]) = IndexOf' (MaybeIndexOf x xs) x xs

Get the first index of a type

type family MaybeIndexOf (a :: k) (l :: [k]) where ...

Get the first index (starting from 1) of a type or 0 if none

Equations

MaybeIndexOf x xs = MaybeIndexOf' 0 x xs

type family Member x xs :: Constraint where ...

Constraint: x member of xs

Equations

Member x xs = MemberAtIndex (IndexOf x xs) x xs

type family InsertAt (n :: Nat) (l :: [k]) (l2 :: [k]) :: [k] where ...

Insert a list at n

Equations

InsertAt 0 xs ys = Concat ys xs

InsertAt n (x ': xs) ys = x ': InsertAt (n - 1) xs ys

type family ReplaceAt (n :: Nat) (l :: [k]) (l2 :: [k]) :: [k] where ...

replace l[n] with l2 (folded)

Equations

ReplaceAt 0 (x ': xs) ys = Concat ys xs

ReplaceAt n (x ': xs) ys = x ': ReplaceAt (n - 1) xs ys

type family IndexesOf (a :: k) (l :: [k]) :: [Nat] where ...

Get all the indexes of a type

Equations

IndexesOf x xs = IndexesOf' 0 x xs

type family ReplaceN (n :: Nat) (t :: k) (l :: [k]) :: [k] where ...

replace a type at offset n in l

Equations

ReplaceN 0 t (x ': xs) = t ': xs

ReplaceN n t (x ': xs) = x ': ReplaceN (n - 1) t xs

type family ReplaceNS (ns :: [Nat]) (t :: k) (l :: [k]) :: [k] where ...

replace types at offsets ns in l

Equations

ReplaceNS '[] t l = l

ReplaceNS (i ': is) t l = ReplaceNS is t (ReplaceN i t l)

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

Complement xs ys

Equations

Complement xs '[] = xs

Complement xs (y : ys) = Complement (Remove y xs) ys

type family RemoveAt (n :: Nat) (l :: [k]) :: [k] where ...

Remove a type at index

Equations

RemoveAt 0 (x ': xs) = xs

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

type family RemoveAt1 (n :: Nat) (l :: [k]) :: [k] where ...

Remove a type at index (0 == don't remove)

Equations

RemoveAt1 0 xs = xs

RemoveAt1 1 (x ': xs) = xs

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

type family Tail (xs :: [k]) :: [k] where ...

Tail of a list

Equations

Tail (x ': xs) = xs

type Constraint = CONSTRAINT LiftedRep

The kind of lifted constraints

type family ConstraintAll1 (f :: k -> Constraint) (xs :: [k]) :: Constraint where ...

Build a list of constraints e.g., ConstraintAll1 Eq '[A,B,C] ==> (Eq A, Eq B, Eq C)

Equations

ConstraintAll1 f '[] = ()

ConstraintAll1 f (x ': xs) = (f x, ConstraintAll1 f xs)