Instantly share code, notes, and snippets.

# Tritlo/Main.hs

Last active January 23, 2018 13:48
Show Gist options
• Save Tritlo/b6479d6912a79ab2d6360340a4783210 to your computer and use it in GitHub Desktop.
Using typed holes to lookup functions with types with non-functional properties.
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 #-} module Main where import Sorting import ONotation -- Here we say that sorted can use at most complexity N^2 and at most memory N^1 -- and that the sort has to be stable. mySort :: Sorted (O(N ^. 2)) (O(N)) True Integer mySort = _ [3,1,2] main :: IO () main = print (sortedBy mySort)
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 import Data.Type.Bool import Data.Type.Equality -- We define a very simplistic O notation, with sufficient expressiveness -- to capture the complexity of a few simple sorting algorithms data AsymptoticPoly = 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 :: AsymptoticPoly) = a type family (^.) (n :: AsymptoticPoly) (m :: Nat) :: AsymptoticPoly where (NLogN a b) ^. n = (NLogN (a * n) (b * n)) type family (*.) (n :: AsymptoticPoly) (m :: AsymptoticPoly) :: AsymptoticPoly where (NLogN a b) *. (NLogN c d) = NLogN (a+c) (b+d) type family OCmp (n :: AsymptoticPoly) (m :: AsymptoticPoly) :: Ordering where OCmp (NLogN a b) (NLogN c d) = If (CmpNat a c == EQ) (CmpNat b d) (CmpNat a c) type family OGEq (n :: AsymptoticPoly) (m :: AsymptoticPoly) :: Bool where OGEq n m = Not (OCmp n m == 'LT) type (>=.) n m = OGEq n m ~ True infix 4 >=. infixl 7 *., ^.
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
 Main.hs:11:10: error: • Found hole: _ :: [Integer] -> Sorted (O ('NLogN 2 0)) (O N) 'True Integer • In the expression: _ In the expression: _ [3, 1, 2] In an equation for ‘mySort’: mySort = _ [3, 1, 2] • Relevant bindings include mySort :: Sorted (O (N ^. 2)) (O N) 'True Integer (bound at Main.hs:11:1) Valid substitutions include mergeSort :: forall a (n :: AsymptoticPoly) (m :: AsymptoticPoly). (Ord a, n >=. O (N *. LogN), m >=. O N) => [a] -> Sorted n m 'True a (imported from ‘Sorting’ at Main.hs:5:1-14 (and originally defined at Sorting.hs:17:1-9)) insertionSort :: forall a (n :: AsymptoticPoly) (m :: AsymptoticPoly). (Ord a, n >=. O (N ^. 2), m >=. O One) => [a] -> Sorted n m 'True a (imported from ‘Sorting’ at Main.hs:5:1-14 (and originally defined at Sorting.hs:26:1-13)) undefined :: forall (a :: TYPE r). GHC.Stack.Types.HasCallStack => a (imported from ‘Prelude’ at Main.hs:3:8-11 (and originally defined in ‘GHC.Err’))
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 #-} module Sorting ( mergeSort, heapSort , quickSort, insertionSort , Sorted, sortedBy) where import ONotation import Data.List (sort) -- We encode in the return type of the sorting function its average complexity, -- memory use and stability. newtype Sorted (avg :: AsymptoticPoly) (mem :: AsymptoticPoly) (stable :: Bool) a = Sorted {sortedBy :: [a]} mergeSort :: (Ord a, n >=. O(N*.LogN), m >=. O(N)) => [a] -> Sorted n m True a mergeSort = Sorted . sort quickSort :: (Ord a, n >=. O(N*.LogN), m >=. O(N)) => [a] -> Sorted n m False a quickSort = Sorted . sort heapSort :: (Ord a, n >=. O(N*.LogN), m >=. O(One)) => [a] -> Sorted n m False a heapSort = Sorted . sort insertionSort :: (Ord a, n >=. O(N^.2), m >=. O(One)) => [a] -> Sorted n m True a insertionSort = Sorted . sort