Using typed holes to lookup functions with types with non-functional properties.

Main.hs

{-# 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)

ONotation.hs

{-# 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 *., ^.

Output.txt

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’))

Sorting.hs

{-# 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