Map parametrized by "named Ord instances"

Instances.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
module Instances where

data Map o k v = Map
  { mapOrder :: k -> k -> Ordering
  , mapImpl :: () -- You'd stick your actual map implementation as another field  here and hide the constructor
  }

data ForgottenMap k v = forall o. ForgottenMap (Map o k v)

newtype Order a = Order { order :: a -> a -> Ordering }

makeMap :: Order k -> [(k, v)] -> (forall o. Map o k v -> r) -> r
makeMap (Order f) kvs c = c (Map f ())

insertMap :: k -> v -> Map o k v -> Map o k v
insertMap k v (Map f x) = Map f x

unionMap :: Map o k v -> Map o k v -> Map o k v
unionMap = error "you'd probably want to implement this :)"

-- You get the idea

usualOrder :: Order Integer
usualOrder = Order compare

oppositeOrder :: Order Integer
oppositeOrder = Order (flip compare)


test1 :: ForgottenMap Integer String
test1 = makeMap usualOrder [(5, "foo"), (7, "bar")] $ \map1 ->
        makeMap oppositeOrder [(8, "baz"), (1, "quux")] $ \map2 ->
        let map3 = insertMap 10 "woof" map1
            map4 = insertMap 11 "meow" map2
        in ForgottenMap (unionMap map3 map3) -- map3 and map3 have the same instance

{-
test2 :: ForgottenMap Integer String
test2 = makeMap usualOrder [(5, "foo"), (7, "bar")] $ \map1 ->
        makeMap oppositeOrder [(8, "baz"), (1, "quux")] $ \map2 ->
        let map3 = insertMap 10 "woof" map1
            map4 = insertMap 11 "meow" map2
        in ForgottenMap (unionMap map3 map4) -- map3 and map4 don't have the same instance, so this is a type error
-}

{-
test3 :: ForgottenMap Integer String
test3 = makeMap usualOrder [(5, "foo"), (7, "bar")] $ \map1 ->
        makeMap usualOrder [(8, "baz"), (1, "quux")] $ \map2 ->
        let map3 = insertMap 10 "woof" map1
            map4 = insertMap 11 "meow" map2
        in ForgottenMap (unionMap map3 map4) -- this also fails, because Haskell doesn't know the two skolems are the same :(
                                             -- You need to bring in various other ingredients (type equality) to make it work,
                                             -- and even then, you need to jump through hoops to convince it every time.
-}