| Copyright | (c) 2020-2021 Tim Emiola |
|---|---|
| License | BSD3 |
| Maintainer | Tim Emiola <adetokunbo@users.noreply.github.com> |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
System.TmpProc.TypeLevel.Sort
Description
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 ... Source #
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 ... Source #
Takes 1 element at a time from a list until the desired length is reached.
Examples
>>>:kind! Take '["a", "b", "c", "d"] 2Take '["a", "b", "c", "d"] 2 :: [Symbol] = '["a", "b"]
type family Drop (xs :: [k]) (n :: Nat) :: [k] where ... Source #
Drops 1 element at a time until the the dropped target is reached.
Examples
>>>:kind! Drop '["a", "b", "c", "d"] 2Drop '["a", "b", "c", "d"] 2 :: [Symbol] = '["c", "d"]
>>>:kind! Drop '["a"] 2Drop '["a"] 2 :: [Symbol] = '[]
type family LengthOf (xs :: [k]) :: Nat where ... Source #
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
type family HalfOf (n :: Nat) :: Nat where ... Source #
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