haskus-system-0.6.0.0: Haskus system programming framework

Safe HaskellSafe
LanguageHaskell2010

Haskus.Utils.Types.List

Description

Utils for type lists

Synopsis

Documentation

type family MapNat (f :: * -> Nat) (xs :: [*]) where ... Source #

Map a type function returning a Nat

Equations

MapNat f '[] = '[] 
MapNat f (x ': xs) = f x ': MapNat f xs 

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

Get the max of a list of Nats

Equations

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

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

Tail of a list

Equations

Tail (x ': xs) = xs 

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

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

Take elements in a list

Equations

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

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

Init of a list

Equations

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

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

Head of a list

Equations

Head (x ': xs) = x 

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

Snoc

Equations

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

type family ReplaceAt (n :: Nat) l l2 where ... Source #

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

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

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 Reverse (l :: [*]) where ... Source #

Reverse a list

Equations

Reverse l = ReverseEx l '[] 

type family RemoveAt (n :: Nat) l where ... Source #

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

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 Concat (xs :: [*]) (ys :: [*]) where ... Source #

Concat two type lists

Equations

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

type family Length xs where ... Source #

Get list length

Equations

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

type family Replicate n s where ... Source #

Replicate

Equations

Replicate 0 s = '[] 
Replicate n s = s ': Replicate (n - 1) s 

type family MapMaybe l where ... Source #

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

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

Check that a type is member of a type list

Equations

IsMember a l = IsMemberEx a l l 

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

Check that a list is a subset of another

Equations

IsSubset l1 l1 = True 
IsSubset l1 l2 = IsSubsetEx l1 l2 l2 

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

Get list indexes

Equations

Indexes xs = IndexesFrom 0 xs 

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

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

Zip two lists

Equations

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

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

Remove a in l

Equations

Filter a '[] = '[] 
Filter a (a ': xs) = Filter a xs 
Filter a (x ': xs) = x ': Filter a xs 

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

Keep only a single value of each type

Equations

Nub '[] = '[] 
Nub (x ': xs) = x ': Nub (Filter x xs) 

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

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

Get the first index of a type

Equations

IndexOf x xs = IndexOfEx x xs xs 

type family MaybeIndexOf a (l :: [*]) where ... Source #

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

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

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

Constraint: x member of xs

type CheckNub l = CheckNubEx l (Nub l) ~ True Source #

Check that a list only contain a value of each type