System.TmpProc.TypeLevel.Sort

Defines type-level combinators for performing a merge sort of type-level lists.

SortSymbols sorts type-level lists of Symbols.

The other exported combinators make it easy to implement type-level merge sort for similar type-level lists.

This is an internal module that provides type-level functions used in various constraints in System.TmpProc.Docker.

Merge sort for Symbols.

type family SortSymbols (xs :: [Symbol]) :: [Symbol] where ...

Sort a list of type-level symbols using merge sort.

Examples

>>> :kind! SortSymbols '["xyz", "def", "abc"]
SortSymbols '["xyz", "def", "abc"] :: [Symbol]
= '["abc", "def", "xyz"]

Equations

SortSymbols '[] = '[]

SortSymbols '[x] = '[x]

SortSymbols '[x, y] = MergeSymbols '[x] '[y]

SortSymbols xs = SortSymbolsStep xs (HalfOf (LengthOf xs))

Sort combinators

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

Takes 1 element at a time from a list until the desired length is reached.

Examples

>>> :kind! Take '[1, 2, 3, 4] 2
Take '[1, 2, 3, 4] 2 :: [Nat]
= '[1, 2]

Equations

Take '[] n = '[]

Take xs 0 = '[]

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

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

Drops 1 element at a time until the the dropped target is reached.

Examples

>>> :kind! Drop '[1, 2, 3, 4] 2
Drop '[1, 2, 3, 4] 2 :: [Nat]
= '[3, 4]

>>> :kind! Drop '[1] 2
Drop '[1] 2 :: [Nat]
= '[]

Equations

Drop '[] n = '[]

Drop xs 0 = xs

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

type family LengthOf (xs :: [k]) :: Nat where ...

Counts a list, 1 element at a time.

Examples

>>> :kind! LengthOf '[1, 2, 3, 4]
LengthOf '[1, 2, 3, 4] :: Nat
= 4

Equations

LengthOf '[] = 0

LengthOf (x ': xs) = 1 + LengthOf xs

type family HalfOf (n :: Nat) :: Nat where ...

Computes the midpoint of a number.

N.B: maximum value that this works for depends on the reduction limit of the type-checker.

Examples

>>> :kind! HalfOf 99
HalfOf 99 :: Nat
= 49

>>> :kind! HalfOf 100
HalfOf 100 :: Nat
= 50

Equations

HalfOf 0 = 0

HalfOf 1 = 1

HalfOf 2 = 1

HalfOf 3 = 1

HalfOf 4 = 2

HalfOf 5 = 2

HalfOf 6 = 3

HalfOf 7 = 3

HalfOf n = HalfOfImpl n 0 n 'LT