main.hs

{-# LANGUAGE DataKinds, TypeOperators, GADTs, KindSignatures, RankNTypes, ScopedTypeVariables #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

import GHC.TypeLits
import Data.Type.Equality(type (==), (:~:)(Refl))

-- Vector of type t and length n.
data Vec t (n :: Nat) where
  VNil  :: Vec t 0
  VCons :: t -> Vec t n -> Vec t (n+1)

-- Conversion to conventional list.
toList :: Vec t n -> [t]
toList VNil = []
toList (VCons x xs) = x:(toList xs)

-- Show instance for convenience.
instance (Show t) => Show (Vec t n) where
  show = show . toList

-- This function inserts an element in an already sorted list.
-- Increases list length by 1.
insert :: (Ord t) => t -> Vec t n -> Vec t (n+1)
insert x VNil = VCons x VNil
insert x (VCons y ys) | x >  y = VCons y (insert x ys)
insert x (VCons y ys) | x <= y = VCons x (insert y ys)

-- Proxy type for kind Nat (see below).
data NatProxy :: Nat -> * where
  NatProxy :: NatProxy n

-- Our insertion sort.              
sort :: (Ord t) => Vec t n -> Vec t n
sort l = sort'
         (NatProxy :: NatProxy n) (NatProxy :: NatProxy n) (NatProxy :: NatProxy 0)
         Refl l VNil

-- Auxiliary function with accumulator.
-- Universal quantification + RankNTypes is required here, as arguments
-- *will* change type in recursive calls.
sort' :: forall l n1 n2 t. (Ord t) =>
-- Proxy values to introduce l, n1, n2 in type scope.
         NatProxy l -> NatProxy n1 -> NatProxy n2 ->
-- Proof of our invariant as a witness that l ~ n1 + n2 (propositional equality).        
         (l :~: n1 + n2) ->
-- Other arguments.          
         Vec t n1 -> Vec t n2 -> Vec t l
-- Pattern-matching on "Refl" brings information that l = n1+n2 into context for type-checking.
sort' p1 p2 p3 Refl VNil acc = acc
sort' p1 p2 p3 Refl (VCons x xs) acc =
     sort'
     (NatProxy :: NatProxy l) (NatProxy :: NatProxy (n1-1)) (NatProxy :: NatProxy (n2+1))
     (Refl :: l :~: (n1-1) + (n2+1))
     xs (insert x acc)

myList = VCons 5 (VCons 4 (VCons 8 (VCons 2 (VCons 12 (VCons 1 VNil)))))

main :: IO ()
main = do
  print myList
  print $ sort myList