Skip to content

Instantly share code, notes, and snippets.

@Tritlo
Last active January 23, 2018 13:48
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Tritlo/b6479d6912a79ab2d6360340a4783210 to your computer and use it in GitHub Desktop.
Save Tritlo/b6479d6912a79ab2d6360340a4783210 to your computer and use it in GitHub Desktop.
Using typed holes to lookup functions with types with non-functional properties.
{-# 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)
{-# 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 *., ^.
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’))
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment