tmp-proc-0.7.0.0: Run 'tmp' processes in integration tests
Copyright(c) 2020-2021 Tim Emiola
LicenseBSD3
MaintainerTim Emiola <adetokunbo@users.noreply.github.com>
Safe HaskellSafe-Inferred
LanguageHaskell2010

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.

Synopsis

Merge sort for Symbols.

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

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

Examples

Expand
>>> :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

Expand
>>> :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 ... Source #

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

Examples

Expand
>>> :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 ... Source #

Counts a list, 1 element at a time.

Examples

Expand
>>> :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 ... 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

Expand
>>> :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