{-# LANGUAGE UndecidableInstances #-}
module Data.DynamicOrd where
import Data.Proxy
import Data.Reflection
import Unsafe.Coerce
newtype O (s :: *) (a :: *) = O { O s a -> a
runO :: a } deriving (Int -> O s a -> ShowS
[O s a] -> ShowS
O s a -> String
(Int -> O s a -> ShowS)
-> (O s a -> String) -> ([O s a] -> ShowS) -> Show (O s a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall s a. Show a => Int -> O s a -> ShowS
forall s a. Show a => [O s a] -> ShowS
forall s a. Show a => O s a -> String
showList :: [O s a] -> ShowS
$cshowList :: forall s a. Show a => [O s a] -> ShowS
show :: O s a -> String
$cshow :: forall s a. Show a => O s a -> String
showsPrec :: Int -> O s a -> ShowS
$cshowsPrec :: forall s a. Show a => Int -> O s a -> ShowS
Show)
newtype OrdDict a = OrdDict { OrdDict a -> a -> a -> Ordering
compare_ :: a -> a -> Ordering }
instance Reifies s (OrdDict a) => Eq (O s a) where
(O a
l) == :: O s a -> O s a -> Bool
== (O a
r) = let cmp :: a -> a -> Ordering
cmp = OrdDict a -> a -> a -> Ordering
forall a. OrdDict a -> a -> a -> Ordering
compare_ (OrdDict a -> a -> a -> Ordering)
-> OrdDict a -> a -> a -> Ordering
forall a b. (a -> b) -> a -> b
$ Proxy s -> OrdDict a
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect (Proxy s
forall k (t :: k). Proxy t
Proxy :: Proxy s)
in case a
l a -> a -> Ordering
`cmp` a
r of
Ordering
EQ -> Bool
True
Ordering
_ -> Bool
False
instance (Eq (O s a), Reifies s (OrdDict a)) => Ord (O s a) where
(O a
l) compare :: O s a -> O s a -> Ordering
`compare` (O a
r) = let cmp :: a -> a -> Ordering
cmp = OrdDict a -> a -> a -> Ordering
forall a. OrdDict a -> a -> a -> Ordering
compare_ (OrdDict a -> a -> a -> Ordering)
-> OrdDict a -> a -> a -> Ordering
forall a b. (a -> b) -> a -> b
$ Proxy s -> OrdDict a
forall k (s :: k) a (proxy :: k -> *). Reifies s a => proxy s -> a
reflect (Proxy s
forall k (t :: k). Proxy t
Proxy :: Proxy s)
in a
l a -> a -> Ordering
`cmp` a
r
withOrd :: (a -> a -> Ordering) -> (forall s. Reifies s (OrdDict a) => O s b) -> b
withOrd :: (a -> a -> Ordering)
-> (forall s. Reifies s (OrdDict a) => O s b) -> b
withOrd a -> a -> Ordering
cmp forall s. Reifies s (OrdDict a) => O s b
v = OrdDict a -> (forall s. Reifies s (OrdDict a) => Proxy s -> b) -> b
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
reify ((a -> a -> Ordering) -> OrdDict a
forall a. (a -> a -> Ordering) -> OrdDict a
OrdDict a -> a -> Ordering
cmp) (O s b -> b
forall s a. O s a -> a
runO (O s b -> b) -> (Proxy s -> O s b) -> Proxy s -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. O s b -> Proxy s -> O s b
forall k k (f :: k -> k -> *) (s :: k) (a :: k).
f s a -> Proxy s -> f s a
asProxyOf O s b
forall s. Reifies s (OrdDict a) => O s b
v)
where
asProxyOf :: f s a -> Proxy s -> f s a
asProxyOf :: f s a -> Proxy s -> f s a
asProxyOf f s a
v' Proxy s
_ = f s a
v'
extractOrd1 :: f (O s a) -> O s (f a)
= f (O s a) -> O s (f a)
forall a b. a -> b
unsafeCoerce
introOrd1 :: f a -> f (O s a)
introOrd1 :: f a -> f (O s a)
introOrd1 = f a -> f (O s a)
forall a b. a -> b
unsafeCoerce
liftOrd1 :: (f (O s a) -> g (O s a))
-> f a -> O s (g a)
liftOrd1 :: (f (O s a) -> g (O s a)) -> f a -> O s (g a)
liftOrd1 f (O s a) -> g (O s a)
f = g (O s a) -> O s (g a)
forall (f :: * -> *) s a. f (O s a) -> O s (f a)
extractOrd1 (g (O s a) -> O s (g a)) -> (f a -> g (O s a)) -> f a -> O s (g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (O s a) -> g (O s a)
f (f (O s a) -> g (O s a)) -> (f a -> f (O s a)) -> f a -> g (O s a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> f (O s a)
forall (f :: * -> *) a s. f a -> f (O s a)
introOrd1
extractOrd2 :: f (O s k) v -> O s (f k v)
= f (O s k) v -> O s (f k v)
forall a b. a -> b
unsafeCoerce
introOrd2 :: f k v -> f (O s k) v
introOrd2 :: f k v -> f (O s k) v
introOrd2 = f k v -> f (O s k) v
forall a b. a -> b
unsafeCoerce