Type.List

Documentation

data Lst (l :: [k])

type family FromLst a where ...

Equations

FromLst (Lst l) = l

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

Instances

type Removed e [e] [e] el ((:) e l ls)

type Removed e [e] [e] el ((:) e l ls) = If [e] ((==) e el l) ls ((:) e l (Removed e [e] [e] el ls))

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

Instances

type RemovedIdx [a] [a] idx ((:) a l ls)

type RemovedIdx [a] [a] idx ((:) a l ls) = If [a] ((==) Nat idx 0) ls ((:) a l (RemovedIdx [a] [a] ((-) idx 1) ls))

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

Instances

type ElAt [l1] l1 idx ((:) l1 l2 ls)

type ElAt [l1] l1 idx ((:) l1 l2 ls) = If l1 ((==) Nat idx 0) l2 (ElAt [l1] l1 ((-) idx 1) ls)

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

Equations

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

SuccMaybe Nothing = Nothing

data Recursive a

Instances

type Index ke * a (Recursive [k] ([] k))

type Index ke * a (Recursive [k] ([] k)) = Nothing Nat

type Index ke * a (Recursive [ke] ((:) ke l ls))

type Index ke * a (Recursive [ke] ((:) ke l ls)) = If (Maybe Nat) ((==) ke a l) (Just Nat 0) (SuccMaybe (Index ke * a (Recursive [ke] ls)))

type family Head lst where ...

Equations

Head '[] = Nothing

Head (a ': as) = Just a

type family Head' lst where ...

Equations

Head' (a ': as) = a

type family UniqueFix lst where ...

Equations

UniqueFix '[] = '[]

UniqueFix lst = Unique lst

type family Reverse' lst lst' where ...

Equations

Reverse' '[] lst = lst

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

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

Equations

Take 0 lst = '[]

Take n (l ': ls) = l ': Take (n - 1) ls

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

Equations

Drop 0 lst = lst

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

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

Equations

Join '[] = '[]

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

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

Equations

Last '[x] = x

Last (x ': xs) = Last xs

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

Equations

Init '[] = '[]

Init '[x] = '[]

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

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

Equations

DropInit '[] = '[]

DropInit '[x] = '[x]

DropInit (x ': xs) = DropInit xs

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

Equations

Replicate 0 a = '[]

Replicate n a = a ': Replicate (n - 1) a

type Zip a b = Zip2 a b

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

Equations

Zip2 (x1 ': xs1) (x2 ': xs2) = (x1, x2) ': Zip2 xs1 xs2

Zip2 l1 l2 = '[]

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

Equations

Zip3 (x1 ': xs1) (x2 ': xs2) (x3 ': xs3) = (x1, x2, x3) ': Zip3 xs1 xs2 xs3

Zip3 l1 l2 l3 = '[]

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

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 Zip5 (l1 :: [*]) (l2 :: [*]) (l3 :: [*]) (l4 :: [*]) (l5 :: [*]) :: [*] where ...

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 Unzip2 (lst :: [*]) :: ([*], [*]) where ...

Equations

Unzip2 '[] = '('[], '[])

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

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

Instances

type PrependAll ([*], [*]) (t1, t2) ((,) [*] [*] l1 l2)

type PrependAll ([*], [*]) (t1, t2) ((,) [*] [*] l1 l2) = (,) [*] [*] ((:) * t1 l1) ((:) * t2 l2)

type PrependAll ([*], [*], [*]) (t1, t2, t3) ((,,) [*] [*] [*] l1 l2 l3)

type PrependAll ([*], [*], [*]) (t1, t2, t3) ((,,) [*] [*] [*] l1 l2 l3) = (,,) [*] [*] [*] ((:) * t1 l1) ((:) * t2 l2) ((:) * t3 l3)

type PrependAll ([*], [*], [*], [*]) (t1, t2, t3, t4) ((,,,) [*] [*] [*] [*] l1 l2 l3 l4)

type PrependAll ([*], [*], [*], [*]) (t1, t2, t3, t4) ((,,,) [*] [*] [*] [*] l1 l2 l3 l4) = (,,,) [*] [*] [*] [*] ((:) * t1 l1) ((:) * t2 l2) ((:) * t3 l3) ((:) * t4 l4)

type PrependAll ([*], [*], [*], [*], [*]) (t1, t2, t3, t4, t5) ((,,,,) [*] [*] [*] [*] [*] l1 l2 l3 l4 l5)

type PrependAll ([*], [*], [*], [*], [*]) (t1, t2, t3, t4, t5) ((,,,,) [*] [*] [*] [*] [*] l1 l2 l3 l4 l5) = (,,,,) [*] [*] [*] [*] [*] ((:) * t1 l1) ((:) * t2 l2) ((:) * t3 l3) ((:) * t4 l4) ((:) * t5 l5)

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

Instances

type Select 1 (t1, t2)

type Select 1 (t1, t2) = t1

type Select 2 (t1, t2)

type Select 2 (t1, t2) = t2

type Select 1 (t1, t2, t3)

type Select 1 (t1, t2, t3) = t1

type Select 2 (t1, t2, t3)

type Select 2 (t1, t2, t3) = t2

type Select 3 (t1, t2, t3)

type Select 3 (t1, t2, t3) = t3

type Select 1 (t1, t2, t3, t4)

type Select 1 (t1, t2, t3, t4) = t1

type Select 2 (t1, t2, t3, t4)

type Select 2 (t1, t2, t3, t4) = t2

type Select 3 (t1, t2, t3, t4)

type Select 3 (t1, t2, t3, t4) = t3

type Select 4 (t1, t2, t3, t4)

type Select 4 (t1, t2, t3, t4) = t4

type Select 1 (t1, t2, t3, t4, t5)

type Select 1 (t1, t2, t3, t4, t5) = t1

type Select 2 (t1, t2, t3, t4, t5)

type Select 2 (t1, t2, t3, t4, t5) = t2

type Select 3 (t1, t2, t3, t4, t5)

type Select 3 (t1, t2, t3, t4, t5) = t3

type Select 4 (t1, t2, t3, t4, t5)

type Select 4 (t1, t2, t3, t4, t5) = t4

type Select 5 (t1, t2, t3, t4, t5)

type Select 5 (t1, t2, t3, t4, t5) = t5

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

Equations

Update 0 a (l ': ls) = a ': ls

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

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

Equations

TakeUntil a '[] = '[]

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

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