extra-exinst.hs

{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeInType            #-}

module Util.Exinst where

import           Data.Kind              (Type)
import           Data.Singletons
import           Data.Singletons.Decide (SDecide)
import           Data.Type.Equality
import           Exinst

s1map :: forall k (f :: k -> Type) (g :: k -> Type)
       . (forall (a :: k). SingI a => f a -> g a)
      -> Some1 f
      -> Some1 g
s1map f s1x = withSome1 s1x (some1 . f)

s1mapSing :: forall k (f :: k -> Type) (g :: k -> Type)
           . (forall (a :: k). SingI a => Sing a -> f a -> g a)
          -> Some1 f
          -> Some1 g
s1mapSing f s1x = withSome1Sing s1x (\sa fa -> some1 $ f sa fa)

s1traverse :: forall k (f :: k -> Type) (g :: k -> Type) m
            . Functor m
           => (forall (a :: k). SingI a => f a -> m (g a))
           -> Some1 f
           -> m (Some1 g)
s1traverse f s1x = withSome1 s1x (fmap some1 . f)

s1traverseSing :: forall k (f :: k -> Type) (g :: k -> Type) m
                . Functor m
               => (forall (a :: k). SingI a => Sing a -> f a -> m (g a))
               -> Some1 f
               -> m (Some1 g)
s1traverseSing f s1x = withSome1Sing s1x (\sa fa -> some1 <$> f sa fa)

withSameSome1 :: forall k (f :: k -> Type) (g :: k -> Type) r
               . SDecide k
              => Some1 f
              -> Some1 g
              -> (forall (a :: k). SingI a => f a -> g a -> r)
              -> Maybe r
withSameSome1 s1f s1g f = withSome1 s1f $ \(fa :: f a1) ->
  withSome1 s1g $ \(ga :: g a2) -> case (sing :: Sing a1) `testEquality` (sing :: Sing a2) of
    Just Refl -> Just $ f fa ga
    Nothing   -> Nothing

withSameSome1Sing :: forall k (f :: k -> Type) (g :: k -> Type) r
                   . SDecide k
                  => Some1 f
                  -> Some1 g
                  -> (forall (a :: k). SingI a => Sing a -> f a -> g a -> r)
                  -> Maybe r
withSameSome1Sing s1f s1g f = withSome1 s1f $ \(fa :: f a1) ->
  withSome1 s1g $ \(ga :: g a2) -> case (sing :: Sing a1) `testEquality` (sing :: Sing a2) of
    Just Refl -> Just $ f (sing :: Sing a1) fa ga
    Nothing   -> Nothing

s1zipWith :: forall k (f :: k -> Type) (g :: k -> Type) (h :: k -> Type)
           . SDecide k
          => (forall (a :: k). SingI a => f a -> g a -> h a)
          -> Some1 f
          -> Some1 g
          -> Maybe (Some1 h)
s1zipWith f s1f s1g = withSameSome1 s1f s1g $ \fa ga -> some1 $ f fa ga

s1zipWithSing :: forall k (f :: k -> Type) (g :: k -> Type) (h :: k -> Type)
               . SDecide k
              => (forall (a :: k). SingI a => Sing a -> f a -> g a -> h a)
              -> Some1 f
              -> Some1 g
              -> Maybe (Some1 h)
s1zipWithSing f s1f s1g = withSameSome1Sing s1f s1g $ \sa fa ga -> some1 $ f sa fa ga

s1zipWithF :: forall k (f :: k -> Type) (g :: k -> Type) (h :: k -> Type) (m :: Type -> Type)
            . (SDecide k, Functor m)
           => (forall (a :: k). SingI a => f a -> g a -> m (h a))
           -> Some1 f
           -> Some1 g
           -> Maybe (m (Some1 h))
s1zipWithF f s1f s1g = withSameSome1 s1f s1g $ \fa ga -> some1 <$> f fa ga

-- | Remove the specified constraint from a function using 'dictN'. These functions
-- is helpful for taking functions on @f a@ and making them suitable to being used
-- as arguments to 'withSome1' and the like

unconstrain0 :: forall k1 (c :: k1 -> Constraint) (f :: k1 -> Type) (a :: k1) (r :: Type)
              . (Dict0 c, SingI a)
             => Proxy c
             -> (c a => f a -> r)
             -> (f a -> r)
unconstrain0 _ k = case dict0 (sing :: Sing a) :: Dict (c a) of
  Dict -> k

unconstrain1 :: forall k1 (c :: Type -> Constraint) (f :: k1 -> Type) (a :: k1) (r :: Type)
             . (Dict1 c f, SingI a)
            => Proxy c
            -> (c (f a) => f a -> r)
            -> (f a -> r)
unconstrain1 _ k = case dict1 (sing :: Sing a) :: Dict (c (f a)) of
  Dict -> k

{-
Example diff of how unconstrainN can simplify code:

-mkSqlCondition (PredicateRep field some1x) = withSome1Sing some1x $
-  \(spt :: Sing pt) args ->
-    case dict0 spt :: Dict (ToSql pt) of
-      Dict -> mkSqlCondition' field args
+mkSqlCondition (PredicateRep field some1x) =
+  withSome1 some1x $ unconstrain0 (Proxy :: Proxy ToSql) (mkSqlCondition' field)
-}

-- | Remove two constraints. This is just an example of how you can "peel" all your
-- constraints away with multiple calls to 'unconstrain'
unconstrainBoth1 :: forall k1 (c1 :: Type -> Constraint) (c2 :: Type -> Constraint) (f :: k1 -> Type) (a :: k1) (r :: Type)
                  . (Dict1 c1 f, Dict1 c2 f, SingI a)
                 => Proxy c1
                 -> Proxy c2
                 -> ((c1 (f a), c2 (f a)) => f a -> r)
                 -> (f a -> r)
unconstrainBoth1 pc1 pc2 k = unconstrain1 pc2 $ unconstrain1 pc1 k

very cool!