typelevel-1.2.3: Useful type level operations (type families and related operators).

Type.List

# Documentation

type family TakeUntil (a :: k) (ls :: [k]) :: [k] where ... Source #

Equations

 TakeUntil a '[] = '[] TakeUntil a (a ': ls) = '[a] TakeUntil a (l ': ls) = l ': TakeUntil a ls

type family Update (n :: Nat) (a :: k) (lst :: [k]) :: [k] where ... Source #

Equations

 Update 0 a (l ': ls) = a ': ls Update n a (l ': ls) = l ': Update (n - 1) a ls

type family Select (n :: Nat) (a :: *) :: * Source #

Instances
 type Select 1 (t1, t2) Source # Instance detailsDefined in Type.List type Select 1 (t1, t2) = t1 type Select 2 (t1, t2) Source # Instance detailsDefined in Type.List type Select 2 (t1, t2) = t2 type Select 1 (t1, t2, t3) Source # Instance detailsDefined in Type.List type Select 1 (t1, t2, t3) = t1 type Select 2 (t1, t2, t3) Source # Instance detailsDefined in Type.List type Select 2 (t1, t2, t3) = t2 type Select 3 (t1, t2, t3) Source # Instance detailsDefined in Type.List type Select 3 (t1, t2, t3) = t3 type Select 1 (t1, t2, t3, t4) Source # Instance detailsDefined in Type.List type Select 1 (t1, t2, t3, t4) = t1 type Select 2 (t1, t2, t3, t4) Source # Instance detailsDefined in Type.List type Select 2 (t1, t2, t3, t4) = t2 type Select 3 (t1, t2, t3, t4) Source # Instance detailsDefined in Type.List type Select 3 (t1, t2, t3, t4) = t3 type Select 4 (t1, t2, t3, t4) Source # Instance detailsDefined in Type.List type Select 4 (t1, t2, t3, t4) = t4 type Select 1 (t1, t2, t3, t4, t5) Source # Instance detailsDefined in Type.List type Select 1 (t1, t2, t3, t4, t5) = t1 type Select 2 (t1, t2, t3, t4, t5) Source # Instance detailsDefined in Type.List type Select 2 (t1, t2, t3, t4, t5) = t2 type Select 3 (t1, t2, t3, t4, t5) Source # Instance detailsDefined in Type.List type Select 3 (t1, t2, t3, t4, t5) = t3 type Select 4 (t1, t2, t3, t4, t5) Source # Instance detailsDefined in Type.List type Select 4 (t1, t2, t3, t4, t5) = t4 type Select 5 (t1, t2, t3, t4, t5) Source # Instance detailsDefined in Type.List type Select 5 (t1, t2, t3, t4, t5) = t5

type family PrependAll (els :: *) (lsts :: k) :: k Source #

Instances
 type PrependAll (t1, t2) ((,) l1 l2 :: ([Type], [Type])) Source # Instance detailsDefined in Type.List type PrependAll (t1, t2) ((,) l1 l2 :: ([Type], [Type])) = (,) (t1 ': l1) (t2 ': l2) type PrependAll (t1, t2, t3) ((,,) l1 l2 l3 :: ([Type], [Type], [Type])) Source # Instance detailsDefined in Type.List type PrependAll (t1, t2, t3) ((,,) l1 l2 l3 :: ([Type], [Type], [Type])) = (,,) (t1 ': l1) (t2 ': l2) (t3 ': l3) type PrependAll (t1, t2, t3, t4) ((,,,) l1 l2 l3 l4 :: ([Type], [Type], [Type], [Type])) Source # Instance detailsDefined in Type.List type PrependAll (t1, t2, t3, t4) ((,,,) l1 l2 l3 l4 :: ([Type], [Type], [Type], [Type])) = (,,,) (t1 ': l1) (t2 ': l2) (t3 ': l3) (t4 ': l4) type PrependAll (t1, t2, t3, t4, t5) ((,,,,) l1 l2 l3 l4 l5 :: ([Type], [Type], [Type], [Type], [Type])) Source # Instance detailsDefined in Type.List type PrependAll (t1, t2, t3, t4, t5) ((,,,,) l1 l2 l3 l4 l5 :: ([Type], [Type], [Type], [Type], [Type])) = (,,,,) (t1 ': l1) (t2 ': l2) (t3 ': l3) (t4 ': l4) (t5 ': l5)

type family Unzip2 (lst :: [*]) :: ([*], [*]) where ... Source #

Equations

 Unzip2 '[] = '('[], '[]) Unzip2 ((x1, x2) ': lst) = PrependAll (x1, x2) (Unzip2 lst)

type family Zip5 (l1 :: [*]) (l2 :: [*]) (l3 :: [*]) (l4 :: [*]) (l5 :: [*]) :: [*] where ... Source #

Equations

 Zip5 (x1 ': xs1) (x2 ': xs2) (x3 ': xs3) (x4 ': xs4) (x5 ': xs5) = (x1, x2, x3, x4, x5) ': Zip5 xs1 xs2 xs3 xs4 xs5 Zip5 l1 l2 l3 l4 l5 = '[]

type family Zip4 (l1 :: [*]) (l2 :: [*]) (l3 :: [*]) (l4 :: [*]) :: [*] where ... Source #

Equations

 Zip4 (x1 ': xs1) (x2 ': xs2) (x3 ': xs3) (x4 ': xs4) = (x1, x2, x3, x4) ': Zip4 xs1 xs2 xs3 xs4 Zip4 l1 l2 l3 l4 = '[]

type family Zip3 (l1 :: [*]) (l2 :: [*]) (l3 :: [*]) :: [*] where ... Source #

Equations

 Zip3 (x1 ': xs1) (x2 ': xs2) (x3 ': xs3) = (x1, x2, x3) ': Zip3 xs1 xs2 xs3 Zip3 l1 l2 l3 = '[]

type family Zip2 (l1 :: [*]) (l2 :: [*]) :: [*] where ... Source #

Equations

 Zip2 (x1 ': xs1) (x2 ': xs2) = (x1, x2) ': Zip2 xs1 xs2 Zip2 l1 l2 = '[]

type Zip a b = Zip2 a b Source #

type family Replicate (n :: Nat) a where ... Source #

Equations

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

type family DropInit (lst :: [k]) :: [k] where ... Source #

Equations

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

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

Equations

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

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

Equations

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

type family Join (lst :: [[k]]) :: [k] where ... Source #

Equations

 Join '[] = '[] Join (lst ': lsts) = Concat lst (Join lsts)

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

Equations

 Drop 0 lst = lst Drop n (l ': ls) = Drop (n - 1) ls

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

Equations

 Take 0 lst = '[] Take n (l ': ls) = l ': Take (n - 1) ls

type family Reverse' lst lst' where ... Source #

Equations

 Reverse' '[] lst = lst Reverse' (l ': ls) lst = Reverse' ls (l ': lst)

type family UniqueFix lst where ... Source #

Equations

 UniqueFix '[] = '[] UniqueFix lst = Unique lst

type family Head' lst where ... Source #

Equations

 Head' (a ': as) = a

type family Head lst where ... Source #

Equations

data Recursive a Source #

Instances
 type Index (a :: ke) (Recursive ([] :: [k]) :: Type) Source # Instance detailsDefined in Type.List type Index (a :: ke) (Recursive ([] :: [k]) :: Type) = (Nothing :: Maybe Nat) type Index (a :: ke) (Recursive (l ': ls) :: Type) Source # Instance detailsDefined in Type.List type Index (a :: ke) (Recursive (l ': ls) :: Type) = If (a == l) (Just 0) (SuccMaybe (Index a (Recursive ls)))

type family SuccMaybe (m :: Maybe Nat) where ... Source #

Equations

 SuccMaybe (Just n) = Just (n + 1) SuccMaybe Nothing = Nothing

type family ElAt (idx :: Nat) (cont :: c) :: l Source #

Instances
 type ElAt idx (l2 ': ls :: [l1]) Source # Instance detailsDefined in Type.List type ElAt idx (l2 ': ls :: [l1]) = If (idx == 0) l2 (ElAt (idx - 1) ls :: l1)

type family RemovedIdx (idx :: Nat) (cont :: c) :: l Source #

Instances
 type RemovedIdx idx (l ': ls :: [a]) Source # Instance detailsDefined in Type.List type RemovedIdx idx (l ': ls :: [a]) = If (idx == 0) ls (l ': (RemovedIdx (idx - 1) ls :: [a]))

type family Removed (el :: e) (cont :: c) :: l Source #

Instances
 type Removed (el :: e) (l ': ls :: [e]) Source # Instance detailsDefined in Type.List type Removed (el :: e) (l ': ls :: [e]) = If (el == l) ls (l ': (Removed el ls :: [e]))

type family FromLst a where ... Source #

Equations

 FromLst (Lst l) = l

data Lst (l :: [k]) Source #