ReflectOrd.hs

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
module ReflectOrd where
import Data.Reflection
import Data.Proxy

newtype Ordable s a = Ordable { unordable :: a }

instance Reifies s (a -> a -> Ordering) => Eq (Ordable s a) where
  Ordable a == Ordable b = reflect (Proxy :: Proxy s) a b == EQ

instance Reifies s (a -> a -> Ordering) => Ord (Ordable s a) where
  compare (Ordable a) (Ordable b) = reflect (Proxy :: Proxy s) a b

f :: forall a x y. (Functor x, Functor y) => (a -> a -> Ordering) -> (forall b. Ord b => x b -> y b) -> x a -> y a
f f g xs =
  reify f $ \(Proxy :: Proxy s) ->
    fmap unordable (g (fmap (\x -> Ordable x :: Ordable s a) xs))

{-# Language DefaultSignatures, RankNTypes, FlexibleContexts, ScopedTypeVariables, UndecidableInstances #-}
module Help where

import Data.Coerce
import Data.Reflection
import Data.Proxy

class Coercible1 f where
  coerce1 :: Coercible a b => f a -> f b
  default coerce1 :: (Coercible (f a) (f b)) => f a -> f b
  coerce1 = coerce

instance Coercible1 [] -- easy to make instances when they are valid

newtype Ordable s a = Ordable { unordable :: a }

instance Reifies s (a -> a -> Ordering) => Eq (Ordable s a) where
  Ordable a == Ordable b = reflect (Proxy :: Proxy s) a b == EQ

instance Reifies s (a -> a -> Ordering) => Ord (Ordable s a) where
  compare (Ordable a) (Ordable b) = reflect (Proxy :: Proxy s) a b

whatisrt ::
  forall a x y.
  (Coercible1 x, Coercible1 y) =>
  (a -> a -> Ordering) ->
  (forall b. Ord b => x b -> y b) ->
  x a -> y a
whatisrt f g xs =
  reify f $ \(Proxy :: Proxy s) ->
    coerce1 (g (coerce1 xs :: x (Ordable s a)))