Created
November 5, 2018 10:14
-
-
Save Tritlo/bf8f4df6a24b1b306d5a478b2c0c425e to your computer and use it in GitHub Desktop.
Type-level complexity annotations in Haskell
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE TypeInType, TypeOperators, TypeFamilies, | |
UndecidableInstances, ConstraintKinds #-} | |
module ONotation where | |
import GHC.TypeLits as L | |
import Data.Type.Bool | |
import Data.Type.Equality | |
-- Simplistic asymptotic polynomials | |
data AsymP = NLogN Nat Nat | |
-- Synonyms for common terms | |
type N = NLogN 1 0 | |
type LogN = NLogN 0 1 | |
type One = NLogN 0 0 | |
-- Just to be able to write it nicely | |
type O (a :: AsymP) = a | |
type family (^.) (n :: AsymP) (m :: Nat) :: AsymP where | |
(NLogN a b) ^. n = NLogN (a L.* n) (b L.* n) | |
type family (*.) (n :: AsymP) (m :: AsymP) :: AsymP where | |
(NLogN a b) *. (NLogN c d) = NLogN (a+c) (b+d) | |
type family OCmp (n :: AsymP) (m :: AsymP) :: Ordering where | |
OCmp (NLogN a b) (NLogN c d) = | |
If (CmpNat a c == EQ) (CmpNat b d) (CmpNat a c) | |
type family OGEq (n :: AsymP) (m :: AsymP) :: Bool where | |
OGEq n m = Not (OCmp n m == 'LT) | |
type (>=.) n m = OGEq n m ~ True |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE TypeInType, TypeOperators, TypeFamilies, | |
TypeApplications #-} | |
module Sorting ( mergeSort, quickSort, insertionSort | |
, Sorted, runSort, module ONotation) where | |
import ONotation | |
import Data.List (insert, sort, partition, foldl') | |
-- Sorted encodes average computational and auxiliary | |
-- memory complexity. The complexities presented | |
-- here are the in-place complexities, and do not match | |
-- the naive but concise implementations included here. | |
newtype Sorted (cpu :: AsymP) (mem :: AsymP) a | |
= Sorted {runSort :: [a]} | |
insertionSort :: (n >=. O(N^.2), m >=. O(One), Ord a) | |
=> [a] -> Sorted n m a | |
insertionSort = Sorted . foldl' (flip insert) [] | |
mergeSort :: (n >=. O(N*.LogN), m >=. O(N), Ord a) | |
=> [a] -> Sorted n m a | |
mergeSort = Sorted . sort | |
quickSort :: (n >=. O(N*.LogN) , m >=. O(LogN), Ord a) | |
=> [a] -> Sorted n m a | |
quickSort (x:xs) = Sorted $ (recr lt) ++ (x:(recr gt)) | |
where (lt, gt) = partition (< x) xs | |
recr = runSort . quickSort @(O(N*.LogN)) @(O(LogN)) | |
quickSort [] = Sorted [] |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment