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 '["a", "b", "c", "d"] 2
Take '["a", "b", "c", "d"] 2 :: [Symbol]
= '["a", "b"]

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 '["a", "b", "c", "d"] 2
Drop '["a", "b", "c", "d"] 2 :: [Symbol]
= '["c", "d"]

>>> :kind! Drop '["a"] 2
Drop '["a"] 2 :: [Symbol]
= '[]

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! CmpNat 4 (LengthOf '[1, 2, 3, 4])
CmpNat 4 (LengthOf '[1, 2, 3, 4]) :: Ordering
= 'EQ

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! CmpNat 49 (HalfOf 99)
CmpNat 49 (HalfOf 99) :: Ordering
= 'EQ

>>> :kind! CmpNat 50 (HalfOf 100)
CmpNat 50 (HalfOf 100) :: Ordering
= 'EQ

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