haskus-utils-types-1.5: Haskus types utility modules

Safe HaskellNone
LanguageHaskell2010

Haskus.Utils.Types.List

Contents

Description

Utils for type lists

Synopsis
  • type family Snoc (xs :: [k]) (x :: k) :: [k] where ...
  • type family Concat (xs :: [k]) (ys :: [k]) :: [k] where ...
  • type family Replicate (n :: Nat) (s :: k) :: [k] where ...
  • type family Zip (l :: [*]) (l2 :: [*]) where ...
  • type family RemoveAt (n :: Nat) (l :: [k]) :: [k] where ...
  • type family RemoveAt1 (n :: Nat) (l :: [k]) :: [k] where ...
  • type family RemoveAtN (ns :: [Nat]) (l :: [k]) :: [k] where ...
  • type family Remove (a :: k) (l :: [k]) :: [k] where ...
  • type family Nub (l :: [k]) :: [k] where ...
  • type family NubHead (l :: [k]) :: [k] where ...
  • type family Head (xs :: [k]) :: k where ...
  • type family Last (xs :: [k]) :: k where ...
  • type family Tail (xs :: [k]) :: [k] where ...
  • type family Init (xs :: [k]) :: [k] where ...
  • type family Take (n :: Nat) (xs :: [k]) :: [k] where ...
  • type family Drop (n :: Nat) (xs :: [k]) :: [k] where ...
  • type family InsertAt (n :: Nat) (l :: [k]) (l2 :: [k]) :: [k] where ...
  • type family ReplaceAt (n :: Nat) (l :: [k]) (l2 :: [k]) :: [k] where ...
  • type family Replace (t1 :: k) (t2 :: k) (l :: [k]) :: [k] where ...
  • type family ReplaceN (n :: Nat) (t :: k) (l :: [k]) :: [k] where ...
  • type family ReplaceNS (ns :: [Nat]) (t :: k) (l :: [k]) :: [k] where ...
  • type family Subset (t :: b) (f :: b) (xs :: [a]) (ys :: [a]) :: b where ...
  • type family SetEq (t :: b) (f :: b) (xs :: [a]) (ys :: [a]) :: b where ...
  • type family CheckMember (a :: k) (l :: [k]) :: Constraint where ...
  • type family CheckMembers (l1 :: [k]) (l2 :: [k]) :: Constraint where ...
  • type family Union (xs :: [k]) (ys :: [k]) :: [k] where ...
  • type family Complement (xs :: [k]) (ys :: [k]) :: [k] where ...
  • type family Product (xs :: [*]) (ys :: [*]) :: [*] where ...
  • type family Member x xs :: Constraint where ...
  • type family Members xs ys :: Constraint where ...
  • type CheckNub (l :: [k]) = CheckNubEx l (Nub l) ~ True
  • type IndexOf (x :: k) (xs :: [k]) = IndexOf' (MaybeIndexOf x xs) x xs
  • type family IndexesOf (a :: k) (l :: [k]) :: [Nat] where ...
  • type family MaybeIndexOf (a :: k) (l :: [k]) where ...
  • type Index (n :: Nat) (l :: [k]) = Index' n l l
  • type family Elem (t :: b) (f :: b) (x :: k) (xs :: [k]) :: b where ...
  • type family MapElem (t :: b) (f :: b) (xs :: [a]) (ys :: [a]) :: [b] where ...
  • type family Reverse (l :: [k]) :: [k] where ...
  • type family Generate (n :: Nat) (m :: Nat) :: [Nat] where ...
  • type family Map (f :: a -> k) (xs :: [a]) :: [k] where ...
  • type family ListMax (xs :: [Nat]) where ...
  • type family ListMin (xs :: [Nat]) where ...
  • type family Length (xs :: [k]) :: Nat where ...
  • type family Indexes (l :: [k]) :: [Nat] where ...
  • type family MapTest (a :: k) (l :: [k]) :: [Nat] where ...

Construction

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

Snoc

Equations

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

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

Concat two type lists

Equations

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

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

Replicate

Equations

Replicate n s = Replicate' s n '[] 

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 

Removal

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

Remove types at several indexes

Equations

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

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

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

Keep only a single value of each type

Equations

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

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

Keep only a single value of the head type

Equations

NubHead '[] = '[] 
NubHead (x ': xs) = x ': Remove x xs 

Sublist

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

Head of a list

Equations

Head (x ': xs) = x 

type family Last (xs :: [k]) :: k where ... Source #

Last of a list

Equations

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

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

Tail of a list

Equations

Tail (x ': xs) = xs 

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

Init of a list

Equations

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

type family Take (n :: Nat) (xs :: [k]) :: [k] where ... Source #

Take elements in a list

Equations

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

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

Drop elements in a list

Equations

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

Insert/replace

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

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 ... 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 :: k) (t2 :: k) (l :: [k]) :: [k] 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 :: Nat) (t :: k) (l :: [k]) :: [k] 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 ReplaceNS (ns :: [Nat]) (t :: k) (l :: [k]) :: [k] where ... Source #

replace types at offsets ns in l

Equations

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

Set operations

type family Subset (t :: b) (f :: b) (xs :: [a]) (ys :: [a]) :: b where ... Source #

Subset test

Equations

Subset t f '[] '[] = t 
Subset t f xs ys = AndMany t f (MapElem t f xs ys) 

type family SetEq (t :: b) (f :: b) (xs :: [a]) (ys :: [a]) :: b where ... Source #

Set equality

Equations

SetEq t f xs ys = And t f (Subset t f xs ys) (Subset t f ys xs) 

type family CheckMember (a :: k) (l :: [k]) :: Constraint where ... Source #

Check that a type is member of a type list

Equations

CheckMember a l = CheckMember' (MaybeIndexOf a l) a l 

type family CheckMembers (l1 :: [k]) (l2 :: [k]) :: Constraint where ... Source #

Check that a list is a subset of another

Equations

CheckMembers '[] l1 = () 
CheckMembers (x ': xs) l2 = CheckMembers' (MaybeIndexOf x l2) x xs (x ': xs) l2 

type family Union (xs :: [k]) (ys :: [k]) :: [k] where ... Source #

Union two lists

Equations

Union xs ys = Nub (Concat xs ys) 

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

Complement xs ys

Equations

Complement xs '[] = xs 
Complement xs (y ': ys) = Complement (Remove y xs) ys 

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

Product of two lists

Equations

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

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

Constraint: x member of xs

Equations

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

type family Members xs ys :: Constraint where ... Source #

Constraint: all the xs are members of ys

Equations

Members '[] ys = () 
Members (x ': xs) ys = (Member x ys, Members xs ys) 

type CheckNub (l :: [k]) = CheckNubEx l (Nub l) ~ True Source #

Check that a list only contain a value of each type

Index operations

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

Get the first index of a type

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

Get all the indexes of a type

Equations

IndexesOf x xs = IndexesOf' 0 x xs 

type family MaybeIndexOf (a :: k) (l :: [k]) 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 Index (n :: Nat) (l :: [k]) = Index' n l l Source #

Indexed access into the list

type family Elem (t :: b) (f :: b) (x :: k) (xs :: [k]) :: b where ... Source #

List membership test

Equations

Elem t f x '[] = f 
Elem t f x (x ': xs) = t 
Elem t f x (y ': xs) = Elem t f x xs 

type family MapElem (t :: b) (f :: b) (xs :: [a]) (ys :: [a]) :: [b] where ... Source #

MapElem t f xs ys = Map (x -> Elem t f x ys) xs

Equations

MapElem t f '[] ys = '[] 
MapElem t f (x ': xs) ys = Elem t f x ys ': MapElem t f xs ys 

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

Reverse a list

Equations

Reverse l = Reverse' l '[] 

Nat list

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 

Others

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

Map a type function

Equations

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

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

Get the max of a list of Nats

Equations

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

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

Get the min of a list of Nats

Equations

ListMin (x ': xs) = Min' x xs 

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

Get list length

Equations

Length xs = Length' 0 xs 

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

Get list indexes

Equations

Indexes xs = IndexesFrom 0 xs 

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

Map to 1 if type equality, 0 otherwise

Equations

MapTest a '[] = '[] 
MapTest a (a ': xs) = 1 ': MapTest a xs 
MapTest a (x ': xs) = 0 ': MapTest a xs