1 {-# LANGUAGE TypeInType, TypeOperators, TypeFamilies,
2 UndecidableInstances, ConstraintKinds #-}
3 module TypeInTypeSubstitutions where
5 import GHC.TypeLits as L
6 import Data.Type.Bool
7 import Data.Type.Equality
8 import Data.List (sort)
11 -- We define a very simplistic O notation, with sufficient expressiveness
12 -- to capture the complexity of a few simple sorting algorithms
13 data AsympPoly = NLogN Nat Nat
15 -- Synonyms for common terms
16 type N = NLogN 1 0
17 type LogN = NLogN 0 1
18 type One = NLogN 0 0
20 -- Just to be able to write it nicely
21 type O (a :: AsympPoly) = a
23 type family (^.) (n :: AsympPoly) (m :: Nat) :: AsympPoly where
24 (NLogN a b) ^. n = (NLogN (a L.* n) (b L.* n))
26 type family (*.) (n :: AsympPoly) (m :: AsympPoly) :: AsympPoly where
27 (NLogN a b) *. (NLogN c d) = NLogN (a+c) (b+d)
29 type family OCmp (n :: AsympPoly) (m :: AsympPoly) :: Ordering where
30 OCmp (NLogN a b) (NLogN c d) = If (CmpNat a c == EQ)
31 (CmpNat b d)
32 (CmpNat a c)
34 type family OGEq (n :: AsympPoly) (m :: AsympPoly) :: Bool where
35 OGEq n m = Not (OCmp n m == 'LT)
37 type (>=.) n m = OGEq n m ~ True
39 infix 4 >=.
40 infixl 7 *., ^.
44 -- Stable sorts must be stable, but unstable can be, but don't need to.
45 type IsStable s = (s || True) ~ True
46 -- We encode in the return type of the sorting function its average complexity,
47 -- memory use and stability.
48 newtype Sorted (cpu :: AsympPoly) -- The minimum operational complexity
49 -- this algorithm satisfies.
50 (mem :: AsympPoly) -- The minimum space complexity this
51 -- algorithm satisfies.
52 (stable :: Bool) -- Whether the sort is stable or not.
53 a -- What was being sorted.
54 = Sorted {sortedBy :: [a]}
56 -- Merge sort is O(N*Log(N)) on average in complexity, so that's the
57 -- minimum complexity we promise to satisfy. Same goes with memory, which is
58 -- O(N), and as we all know, mergesort is a stable sorting algoritm.
59 mergeSort :: (Ord a, n >=. O(N*.LogN), m >=. O(N), IsStable s) =>
60 [a] -> Sorted n m s a
61 mergeSort = Sorted . sort
63 insertionSort :: (Ord a, n >=. O(N^.2), m >=. O(One), IsStable s) =>
64 [a] -> Sorted n m s a
65 insertionSort = Sorted . sort
67 -- Note that we don't actually check the complexity (as evidenced by them all
68 -- being implemented with sort, a smooth applicative merge sort). With more
69 -- dependent types however, some of these properties might be verifiable.
70 quickSort :: (Ord a, n >=. O(N*.LogN), m >=. O(N)) => [a] -> Sorted n m False a
71 quickSort = Sorted . sort
73 heapSort :: (Ord a, n >=. O(N*.LogN), m >=. O(One)) => [a] -> Sorted n m False a
74 heapSort = Sorted . sort
76 -- Here we say that sorted can use at most operational complexity O(N^2), space
77 -- complexity of at most (O(N)) and that it should be stable.
78 mySortA :: Sorted (O(N^.2)) (O(N)) True Integer
79 mySortA = _a [3,1,2]
81 mySortB :: Sorted (O(N*.LogN)) (O(N)) False Integer
82 mySortB = _b [3,1,2]
84 mySortC :: Sorted (O(N*.LogN)) (O(One)) False Integer
85 mySortC = _c [3,1,2]
87 main :: IO ()
88 main = print (sortedBy mySortA)