Haskus.Utils.Types.List

Utils for type lists

Documentation

type family Map (f :: a -> k) (xs :: [a]) where ...

Map a type function

Equations

Map f '[] = '[]

Map f (x ': xs) = f x ': Map f xs

type family Max (xs :: [Nat]) where ...

Get the max of a list of Nats

Equations

Max (x ': xs) = Max' x xs

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

Tail of a list

Equations

Tail (x ': xs) = xs

type family Drop (n :: Nat) (xs :: [*]) where ...

Drop elements in a list

Equations

Drop 0 xs = xs

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

type family Take (n :: Nat) (xs :: [*]) where ...

Take elements in a list

Equations

Take 0 xs = '[]

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

type family Init (xs :: [*]) where ...

Init of a list

Equations

Init '[x] = '[]

Init (x ': xs) = x ': Init xs

type family Head (xs :: [*]) where ...

Head of a list

Equations

Head (x ': xs) = x

type family Snoc (xs :: [*]) x where ...

Snoc

Equations

Snoc '[] x = '[x]

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

type family InsertAt (n :: Nat) l l2 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 l2 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 Replace t1 t2 l where ...

replace a type by another in l

Equations

Replace t1 t2 '[] = '[]

Replace t1 t2 (t1 ': xs) = t2 ': Replace t1 t2 xs

Replace t1 t2 (x ': xs) = x ': Replace t1 t2 xs

type family ReplaceN n t l 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 t l 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 Reverse (l :: [*]) where ...

Reverse a list

Equations

Reverse l = Reverse' l '[]

type family RemoveAt (n :: Nat) l 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 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 RemoveAtN (ns :: [Nat]) l where ...

Remove types at several indexes

Equations

RemoveAtN '[] xs = xs

RemoveAtN (i ': is) xs = RemoveAtN is (RemoveAt i xs)

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

Concat two type lists

Equations

Concat '[] '[] = '[]

Concat '[] ys = ys

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

type family Length xs where ...

Get list length

Equations

Length xs = Length' 0 xs

type family Replicate n s where ...

Replicate

Equations

Replicate n s = Replicate' s n '[]

type family MapMaybe l where ...

Apply Maybe to all the elements of the list

Equations

MapMaybe '[] = '[]

MapMaybe (x ': xs) = Maybe x ': MapMaybe xs

type family Generate (n :: Nat) (m :: Nat) :: [Nat] where ...

Generate a list of Nat [n..m-1]

Equations

Generate n n = '[]

Generate n m = n ': Generate (n + 1) m

type family IsMember a (l :: [*]) :: Bool where ...

Check that a type is member of a type list

Equations

IsMember a l = IsMember' l a l

type family IsSubset l1 l2 :: Bool where ...

Check that a list is a subset of another

Equations

IsSubset l1 l1 = True

IsSubset l1 l2 = IsSubset' l2 l1 l2

type family Indexes (l :: [*]) where ...

Get list indexes

Equations

Indexes xs = IndexesFrom 0 xs

type family MapTest a (l :: [*]) where ...

Map to 1 if type equality, 0 otherwise

Equations

MapTest a '[] = '[]

MapTest a (a ': xs) = Proxy 1 ': MapTest a xs

MapTest a (x ': xs) = Proxy 0 ': MapTest a xs

type family Zip (l :: [*]) (l2 :: [*]) where ...

Zip two lists

Equations

Zip '[] xs = '[]

Zip xs '[] = '[]

Zip (x ': xs) (y ': ys) = (x, y) ': Zip xs ys

type family Filter a (l :: [*]) where ...

Remove a in l

Equations

Filter a '[] = '[]

Filter a (a ': as) = Filter a as

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

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

Keep only a single value of each type

Equations

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

type family NubHead (l :: [*]) where ...

Keep only a single value of the head type

Equations

NubHead '[] = '[]

NubHead (x ': xs) = x ': Filter x xs

type family IndexOf a (l :: [*]) :: Nat where ...

Get the first index of a type

Equations

IndexOf x xs = IndexOf' x xs xs

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

Get all the indexes of a type

Equations

IndexesOf x xs = IndexesOf' 0 x xs

type family MaybeIndexOf a (l :: [*]) 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 Index (n :: Nat) (l :: [*]) where ...

Indexed access into the list

Equations

Index 0 (x ': xs) = x

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

type family Union (xs :: [*]) (ys :: [*]) where ...

Union two lists

Equations

Union xs ys = Nub (Concat xs ys)

type Member x xs = (IsMember x xs ~ True, x ~ Index (IndexOf x xs) xs, KnownNat (IndexOf x xs))

Constraint: x member of xs

type CheckNub (l :: [*]) = CheckNubEx l (Nub l) ~ True

Check that a list only contain a value of each type