TaggingDefs.hs

{-# LANGUAGE FlexibleContexts, FlexibleInstances, FunctionalDependencies, PolyKinds, UndecidableSuperClasses #-}
{-# LANGUAGE Rank2Types, TypeApplications, QuantifiedConstraints #-}
module TaggingDefs
( Tagged(..)
, Untag
, Retag
, untag
, untag'
, retag
, retag'
) where

import Data.Constraint
import Data.Coerce

-- | Use this as a blanket term instead of the constraint @c@
-- when you want to differentiate between different implementations.
-- Demonstrating on an example, an instance for @Tagged "t" Monoid a@
-- would provide the newtype that actually implements the Monoid
-- instance we want to use for plucking the constraint as @Fulfillment "t" Monoid a@.
class (Coercible (Fulfillment tag c a) a, c (Fulfillment tag c a))
    => Tagged (tag :: k2) (c :: k1 -> Constraint) (a :: k1) where
    type Fulfillment tag c a :: k1

-- The arguments tag and c are for type deduction only, thus phantom.
-- The last is the argument used for the constraint, and nominal
class Coercible a b => Untag (tag :: k1) (c :: Constraint) (a :: *) (b :: *) | a -> tag, a -> c, a -> b
class Coercible a b => Retag (tag :: k1) (c :: Constraint) (a :: *) (b :: *) | a -> tag, a -> c, a -> b

untag' :: (Untag tag c u a, Coercible (t u) (t a))
        => t u -> t a
untag' = coerce
{-# INLINE untag' #-}

untag :: (Untag tag c u a) => u -> a
untag = coerce
{-# INLINE untag #-}

retag' :: (Retag tag c u a, Coercible (t u) (t a))
        => t u -> t a
retag' = coerce
{-# INLINE retag' #-}

retag :: (Retag tag c u a) => u -> a
retag = coerce
{-# INLINE retag #-}

TaggingExample.hs

{-# LANGUAGE DerivingVia, FlexibleInstances, TypeApplications, FlexibleContexts, PolyKinds, QuantifiedConstraints, UndecidableInstances #-}
module TaggingExample
( module TaggingExample ) where

import TaggingDefs
import TaggingInstances
import Control.Monad.IO.Class
import Data.Coerce


-- First up, an example how to pluck constraints of existing typeclasses, by example of Semigroup

-- this newtype implements Num a => Semigroup a by multiplication
newtype Multiply a = Multiply { runMult :: a }
instance Num a => Semigroup (Multiply a) where
    a <> b = Multiply $ runMult a * runMult b
-- this newtype implements Num a => Semigroup a by addition
newtype Adding a = Adding { runAdd :: a }
instance Num a => Semigroup (Adding a) where
    a <> b = Adding $ runAdd a + runAdd b

-- and more boilerplate. These first two should probably be in TaggingInstances...
tagSemigroup :: forall tag a. Retag0 tag Semigroup a -> a
tagSemigroup = coerce
untagSemigroup :: forall tag a. Untag0 tag Semigroup a -> a
untagSemigroup = coerce
-- boilerplate for Multiply
runMulitply :: forall a. (Semigroup `Via0` Multiply) a -> a
runMulitply = coerce
runMulitply' :: forall tag a. Untag0 tag Semigroup ((Semigroup `Via0` Multiply) a) -> a
runMulitply' = runMulitply . untagSemigroup
-- boilderplate for Adding
runAdding :: forall a. (Semigroup `Via0` Adding) a -> a
runAdding = coerce
runAdding' :: forall tag a. Untag0 tag Semigroup ((Semigroup `Via0` Adding) a) -> a
runAdding' = runAdding . untagSemigroup

-- example computation we want to pluck
untagged :: (Semigroup a) => a -> a -> a
untagged x y = x <> y

-- a few helper coercions. Most of the helper functions could be generated by template haskell
untagBinFun' :: forall tag c a. (Untag0 tag c a -> Untag0 tag c a -> Untag0 tag c a)
             -> a -> a -> a
untagBinFun' = coerce

tagBinFun' :: forall tag c a. (Retag0 tag c a -> Retag0 tag c a -> Retag0 tag c a)
           -> a -> a -> a
tagBinFun' = coerce

tagged :: (Tagged "tag1" Semigroup a) => a -> a -> a
tagged = tagBinFun' @"tag1" @Semigroup untagged

tagged2 :: (Tagged "tag2" Semigroup a) => a -> a -> a
tagged2 = tagBinFun' @"tag2" @Semigroup untagged

combined :: (Tagged "tag1" Semigroup a, Tagged "tag2" Semigroup a)
         => a -> a -> (a, a)
combined x y = (tagged x y, tagged2 x y)

type RRTagged a = a -> a -> (a, a)
runtagged :: Num a => a -> a -> (a, a)
runtagged = rB $ uS @"tag1" $ rA $ uS @"tag2" $ combined where
    -- not sure show to cut down on this type of usage. When using it for Monads, one probably wants to use
    -- it for full programs (i.e types @(Monad m, c m) => m r@ only anyway, so it's not that bad
    uS :: forall tag a. RRTagged (Untag0 tag Semigroup a) -> RRTagged a
    uS = coerce
    rA :: RRTagged ((Semigroup `Via0` Adding) x) -> RRTagged x
    rA = coerce
    rB :: RRTagged ((Semigroup `Via0` Multiply) x) -> RRTagged x
    rB = coerce

-- Secondly, an example of adding an additional class

-- example how to use it for monadic computations
-- a class of constraint we want to use in our program
-- note that this doesn't have a Monad m superclass, which simplifies the treatment later.
-- In reality, one could use the alias @type Console' m = (Monad m, Console m)@ as the constraint to
-- use in consumer code without putting more strain on the boilerplate code.
class Console m where
    getCChar :: m Char

-- the following instances are purely boilerplate code, could auto-generate this
-- first up, instances needed for untagging (Tagged tag Console m => Console m)
deriving via (f :: * -> *) instance (Console f) => Console (Untag1 tag c f)
instance (Tagged' (t1 == t2) t1 Console f) => Tagged t1 Console (Untag1 t2 c f) where
    type Fulfillment t1 Console (Untag1 t2 c f) = Fulfillment' (t1 == t2) t1 Console f
instance Console f => Tagged' 'True t1 Console f where
    type Fulfillment' 'True t1 Console f = f
instance (Tagged t1 Console f) => Tagged' 'False t1 Console f where
    type Fulfillment' 'False t1 Console f = Fulfillment t1 Console f
-- next the instances for tagging (Console m => Tagged tag Console m)
deriving via (f :: * -> *)
    instance {-# OVERLAPPABLE #-} Console f => Console (Retag1 tag c f)
deriving via (Fulfillment tag Console f)
    instance {-# OVERLAPPING #-} (Tagged tag Console f) => Console (Retag1 tag Console f)
-- lastly the instances for plucking the constraint with an implementation
deriving via (f :: * -> *)
    instance {-# OVERLAPPABLE #-} (forall b. Coercible (t f b) (f b), Console f) => Console (Via1 c t f)
deriving via ((t :: (* -> *) -> (* -> *)) f)
    instance {-# OVERLAPPING #-} (Console (t f)) => Console (Via1 Console t f)

-- the following methods are also "standard" to implement and use, could also auto-generate those (ref. tagSemigroup)
tagConsole :: forall tag m a. Retag1 tag Console m a -> m a
tagConsole = coerce
untagConsole :: forall tag m a. Untag1 tag Console m a -> m a
untagConsole = coerce

-- an "implementation" of the constraint via @MonadIO m => Console m@
newtype ConsoleIO m a = ConsoleIO (m a)
instance MonadIO m => Console (ConsoleIO m) where
    getCChar = ConsoleIO $ liftIO $ getChar

-- the following methods are "standard" per "implementation" (ref. runAdding)
runConsoleIO :: forall m a. (Console `Via1` ConsoleIO) m a -> m a
runConsoleIO = coerce
runConsoleIO' :: forall tag m a. Untag1 tag Console ((Console `Via1` ConsoleIO) m) a -> m a
runConsoleIO' = runConsoleIO . untagConsole

-- example generic program
program :: (Monad m, Console m) => m Char
program = getCChar >> getCChar
-- use ConsoleIO to run the program
programPlucked :: (MonadIO m) => m Char
programPlucked = runConsoleIO program
-- just uselessly tag and use runConsoleIO', then instantiate to IO
programPluckedIO :: IO Char
programPluckedIO = runConsoleIO' @"tag" $ tagConsole @"tag" $ program

TaggingInstances.hs

{-# LANGUAGE DerivingVia, FunctionalDependencies, FlexibleContexts, FlexibleInstances, ExplicitNamespaces #-}
{-# LANGUAGE PolyKinds, UndecidableSuperClasses, RoleAnnotations, UndecidableInstances, QuantifiedConstraints #-}
module TaggingInstances
( Untag0(..)
, Retag0(..)
, Untag1(..)
, Retag1(..)
, Via0(..)
, Via1(..)
, Tagged'(..)
, type (==)
) where

import Control.Monad.IO.Class
-- import Control.Monad.State.Class
import Data.Constraint
import Data.Coerce
import Data.Type.Equality

import TaggingDefs

-- Helper class for instance resolution
class (Coercible (Fulfillment' b tag c a) a, c (Fulfillment' b tag c a))
    => Tagged' (b :: Bool) (tag :: k2) (c :: k1 -> Constraint) (a :: k1) where
    type Fulfillment' b tag c a :: k1

-- data types for constraints of kind * -> Constraints
newtype Untag0 (tag :: k1) (c :: * -> Constraint) (a :: *) = Untag0 { runUntag0 :: a }
type role Untag0 phantom phantom nominal
instance Untag tag (c a) (Untag0 tag c a) a

newtype Retag0 (tag :: k1) (c :: * -> Constraint) (a :: *) = Retag0 { runRetag0 :: a }
type role Retag0 phantom phantom nominal
instance Retag tag (c a) (Retag0 tag c a) a

-- untagging for kind * -> Constraint
deriving via (a :: *) instance (Num a) => Num (Untag0 tag c a)
instance (Tagged' (t1 == t2) t1 Num a) => Tagged t1 Num (Untag0 t2 c a) where
    type Fulfillment t1 Num (Untag0 t2 c a) = Fulfillment' (t1 == t2) t1 Num a
instance Num a => Tagged' 'True t1 Num a where
    type Fulfillment' 'True t1 Num a = a
instance (Tagged t1 Num a) => Tagged' 'False t1 Num a where
    type Fulfillment' 'False t1 Num a = Fulfillment t1 Num a

deriving via (a :: *) instance (Enum a) => Enum (Untag0 tag c a)
instance (Tagged' (t1 == t2) t1 Enum a) => Tagged t1 Enum (Untag0 t2 c a) where
    type Fulfillment t1 Enum (Untag0 t2 c a) = Fulfillment' (t1 == t2) t1 Enum a
instance Enum a => Tagged' 'True t1 Enum a where
    type Fulfillment' 'True t1 Enum a = a
instance (Tagged t1 Enum a) => Tagged' 'False t1 Enum a where
    type Fulfillment' 'False t1 Enum a = Fulfillment t1 Enum a

deriving via (a :: *) instance (Semigroup a) => Semigroup (Untag0 tag c a)
instance (Tagged' (t1 == t2) t1 Semigroup a) => Tagged t1 Semigroup (Untag0 t2 c a) where
    type Fulfillment t1 Semigroup (Untag0 t2 c a) = Fulfillment' (t1 == t2) t1 Semigroup a
instance Semigroup a => Tagged' 'True t1 Semigroup a where
    type Fulfillment' 'True t1 Semigroup a = a
instance (Tagged t1 Semigroup a) => Tagged' 'False t1 Semigroup a where
    type Fulfillment' 'False t1 Semigroup a = Fulfillment t1 Semigroup a

deriving via (a :: *) instance (Monoid a) => Monoid (Untag0 tag c a)
instance (Tagged' (t1 == t2) t1 Monoid a) => Tagged t1 Monoid (Untag0 t2 c a) where
    type Fulfillment t1 Monoid (Untag0 t2 c a) = Fulfillment' (t1 == t2) t1 Monoid a
instance Monoid a => Tagged' 'True t1 Monoid a where
    type Fulfillment' 'True t1 Monoid a = a
instance (Tagged t1 Monoid a) => Tagged' 'False t1 Monoid a where
    type Fulfillment' 'False t1 Monoid a = Fulfillment t1 Monoid a

-- tagging for kind * -> Constraint
deriving via (a :: *)
    instance {-# OVERLAPPABLE #-} Num a => Num (Retag0 tag c a)
deriving via (Fulfillment tag Num a)
    instance {-# OVERLAPPING #-} (Tagged tag Num a) => Num (Retag0 tag Num a)

deriving via (a :: *)
    instance {-# OVERLAPPABLE #-} Enum a => Enum (Retag0 tag c a)
deriving via (Fulfillment tag Enum a)
    instance {-# OVERLAPPING #-} (Tagged tag Enum a) => Enum (Retag0 tag Enum a)

deriving via (a :: *)
    instance {-# OVERLAPPABLE #-} Semigroup a => Semigroup (Retag0 tag c a)
deriving via (Fulfillment tag Semigroup a)
    instance {-# OVERLAPPING #-} (Tagged tag Semigroup a) => Semigroup (Retag0 tag Semigroup a)

deriving via (a :: *)
    instance {-# OVERLAPPABLE #-} Monoid a => Monoid (Retag0 tag c a)
deriving via (Fulfillment tag Monoid a)
    instance {-# OVERLAPPING #-} (Tagged tag Monoid a) => Semigroup (Retag0 tag Monoid a)
deriving via (Fulfillment tag Monoid a)
    instance {-# OVERLAPPING #-} (Tagged tag Monoid a) => Monoid (Retag0 tag Monoid a)

-- via for * -> Constraint
-- why, yes this suffers from O(n^2) problem (in the nesting depth), I don't see a way around it.
newtype Via0 (c :: * -> Constraint) (t :: * -> *) (a :: *) = Via0 { runVia0 :: t a }

deriving via (a :: *)
    instance {-# OVERLAPPABLE #-} (Coercible (t a) a, Tagged tag c a) => Tagged tag c (Via0 c t a)

deriving via (a :: *)
    instance {-# OVERLAPPABLE #-} (Coercible (t a) a, Num a) => Num (Via0 c t a)
deriving via ((t :: * -> *) a)
    instance {-# OVERLAPPING #-} (Num (t a)) => Num (Via0 Num t a)

deriving via (a :: *)
    instance {-# OVERLAPPABLE #-} (Coercible (t a) a, Enum a) => Enum (Via0 c t a)
deriving via ((t :: * -> *) a)
    instance {-# OVERLAPPING #-} (Enum (t a)) => Enum (Via0 Enum t a)

deriving via (a :: *)
    instance {-# OVERLAPPABLE #-} (Coercible (t a) a, Semigroup a) => Semigroup (Via0 c t a)
deriving via ((t :: * -> *) a)
    instance {-# OVERLAPPING #-} (Semigroup (t a)) => Semigroup (Via0 Semigroup t a)

deriving via (a :: *)
    instance {-# OVERLAPPABLE #-} (Coercible (t a) a, Monoid a) => Monoid (Via0 c t a)
deriving via ((t :: * -> *) a)
    instance {-# OVERLAPPING #-} (Semigroup (t a)) => Semigroup (Via0 Monoid t a)
deriving via ((t :: * -> *) a)
    instance {-# OVERLAPPING #-} (Monoid (t a)) => Monoid (Via0 Monoid t a)

-- data types for constraints of kind (k -> *) -> Constraints
newtype Untag1 (tag :: k1) (c :: (k2 -> *) -> Constraint) (m :: k2 -> *) (a :: k2) = Untag1 { runUntag1 :: m a }
type role Untag1 phantom phantom nominal nominal
instance Untag tag (c m) (Untag1 tag c m a) (m a)

newtype Retag1 (tag :: k1) (c :: (k2 -> *) -> Constraint) (m :: k2 -> *) (a :: k2) = Retag1 { runRetag1 :: m a }
type role Retag1 phantom phantom nominal nominal
instance Retag tag (c m) (Retag1 tag c m a) (m a)

-- untagging for kind (k -> *) -> Constraint
-- functor
deriving via (f :: * -> *) instance (Functor f) => Functor (Untag1 tag c f)
instance (Tagged' (t1 == t2) t1 Functor f) => Tagged t1 Functor (Untag1 t2 c f) where
    type Fulfillment t1 Functor (Untag1 t2 c f) = Fulfillment' (t1 == t2) t1 Functor f

instance Functor f => Tagged' 'True t1 Functor f where
    type Fulfillment' 'True t1 Functor f = f

instance (Tagged t1 Functor f) => Tagged' 'False t1 Functor f where
    type Fulfillment' 'False t1 Functor f = Fulfillment t1 Functor f

-- Applicative
deriving via (f :: * -> *) instance (Applicative f) => Applicative (Untag1 tag c f)
instance (Tagged' (t1 == t2) t1 Applicative f) => Tagged t1 Applicative (Untag1 t2 c f) where
    type Fulfillment t1 Applicative (Untag1 t2 c f) = Fulfillment' (t1 == t2) t1 Applicative f

instance Applicative f => Tagged' 'True t1 Applicative f where
    type Fulfillment' 'True t1 Applicative f = f

instance (Tagged t1 Applicative f) => Tagged' 'False t1 Applicative f where
    type Fulfillment' 'False t1 Applicative f = Fulfillment t1 Applicative f

-- Monad
deriving via (f :: * -> *) instance (Monad f) => Monad (Untag1 tag c f)
instance (Tagged' (t1 == t2) t1 Monad f) => Tagged t1 Monad (Untag1 t2 c f) where
    type Fulfillment t1 Monad (Untag1 t2 c f) = Fulfillment' (t1 == t2) t1 Monad f

instance Monad f => Tagged' 'True t1 Monad f where
    type Fulfillment' 'True t1 Monad f = f

instance (Tagged t1 Monad f) => Tagged' 'False t1 Monad f where
    type Fulfillment' 'False t1 Monad f = Fulfillment t1 Monad f

-- MonadIO
deriving via (f :: * -> *) instance (MonadIO f) => MonadIO (Untag1 tag c f)
instance (Tagged' (t1 == t2) t1 MonadIO f) => Tagged t1 MonadIO (Untag1 t2 c f) where
    type Fulfillment t1 MonadIO (Untag1 t2 c f) = Fulfillment' (t1 == t2) t1 MonadIO f

instance MonadIO f => Tagged' 'True t1 MonadIO f where
    type Fulfillment' 'True t1 MonadIO f = f

instance (Tagged t1 MonadIO f) => Tagged' 'False t1 MonadIO f where
    type Fulfillment' 'False t1 MonadIO f = Fulfillment t1 MonadIO f

-- tagging for kind (k -> *) -> Constraint
deriving via (f :: * -> *)
    instance {-# OVERLAPPABLE #-} Functor f => Functor (Retag1 tag c f)
deriving via (Fulfillment tag Functor f)
    instance {-# OVERLAPPING #-} (Tagged tag Functor f) => Functor (Retag1 tag Functor f)

deriving via (f :: * -> *)
    instance {-# OVERLAPPABLE #-} Applicative f => Applicative (Retag1 tag c f)
deriving via (Fulfillment tag Applicative f)
    instance {-# OVERLAPPING #-} (Tagged tag Applicative f) => Functor (Retag1 tag Applicative f)
deriving via (Fulfillment tag Applicative f)
    instance {-# OVERLAPPING #-} (Tagged tag Applicative f) => Applicative (Retag1 tag Applicative f)

deriving via (f :: * -> *)
    instance {-# OVERLAPPABLE #-} Monad f => Monad (Retag1 tag c f)
deriving via (Fulfillment tag Monad f)
    instance {-# OVERLAPPING #-} (Tagged tag Monad f) => Functor (Retag1 tag Monad f)
deriving via (Fulfillment tag Monad f)
    instance {-# OVERLAPPING #-} (Tagged tag Monad f) => Applicative (Retag1 tag Monad f)
deriving via (Fulfillment tag Monad f)
    instance {-# OVERLAPPING #-} (Tagged tag Monad f) => Monad (Retag1 tag Monad f)

deriving via (f :: * -> *)
    instance {-# OVERLAPPABLE #-} MonadIO f => MonadIO (Retag1 tag c f)
deriving via (Fulfillment tag MonadIO f)
    instance {-# OVERLAPPING #-} (Tagged tag MonadIO f) => Functor (Retag1 tag MonadIO f)
deriving via (Fulfillment tag MonadIO f)
    instance {-# OVERLAPPING #-} (Tagged tag MonadIO f) => Applicative (Retag1 tag MonadIO f)
deriving via (Fulfillment tag MonadIO f)
    instance {-# OVERLAPPING #-} (Tagged tag MonadIO f) => Monad (Retag1 tag MonadIO f)
deriving via (Fulfillment tag MonadIO f)
    instance {-# OVERLAPPING #-} (Tagged tag MonadIO f) => MonadIO (Retag1 tag MonadIO f)

-- via for (k -> *) -> Constraint
newtype Via1 (c :: (k -> *) -> Constraint) (t :: (k -> *) -> (k -> *)) (f :: k -> *) (b :: k) = Via1 { runVia1 :: (t f) b }

deriving via (f :: * -> *)
    instance (Coercible (t f) f, Tagged tag c f) => Tagged tag c (Via1 c t f)

deriving via (f :: * -> *)
    instance {-# OVERLAPPABLE #-} (forall b. Coercible (t f b) (f b), Functor f) => Functor (Via1 c t f)
deriving via ((t :: (* -> *) -> (* -> *)) f)
    instance {-# OVERLAPPING #-} (Functor (t f)) => Functor (Via1 Functor t f)

deriving via (f :: * -> *)
    instance {-# OVERLAPPABLE #-} (forall b. Coercible (t f b) (f b), Applicative f) => Applicative (Via1 c t f)
deriving via ((t :: (* -> *) -> (* -> *)) f)
    instance {-# OVERLAPPING #-} (Functor (t f)) => Functor (Via1 Applicative t f)
deriving via ((t :: (* -> *) -> (* -> *)) f)
    instance {-# OVERLAPPING #-} (Applicative (t f)) => Applicative (Via1 Applicative t f)

deriving via (f :: * -> *)
    instance {-# OVERLAPPABLE #-} (forall b. Coercible (t f b) (f b), Monad f) => Monad (Via1 c t f)
deriving via ((t :: (* -> *) -> (* -> *)) f)
    instance {-# OVERLAPPING #-} (Functor (t f)) => Functor (Via1 Monad t f)
deriving via ((t :: (* -> *) -> (* -> *)) f)
    instance {-# OVERLAPPING #-} (Applicative (t f)) => Applicative (Via1 Monad t f)
deriving via ((t :: (* -> *) -> (* -> *)) f)
    instance {-# OVERLAPPING #-} (Monad (t f)) => Monad (Via1 Monad t f)

deriving via (f :: * -> *)
    instance {-# OVERLAPPABLE #-} (forall b. Coercible (t f b) (f b), MonadIO f) => MonadIO (Via1 c t f)
deriving via ((t :: (* -> *) -> (* -> *)) f)
    instance {-# OVERLAPPING #-} (Functor (t f)) => Functor (Via1 MonadIO t f)
deriving via ((t :: (* -> *) -> (* -> *)) f)
    instance {-# OVERLAPPING #-} (Applicative (t f)) => Applicative (Via1 MonadIO t f)
deriving via ((t :: (* -> *) -> (* -> *)) f)
    instance {-# OVERLAPPING #-} (Monad (t f)) => Monad (Via1 MonadIO t f)
deriving via ((t :: (* -> *) -> (* -> *)) f)
    instance {-# OVERLAPPING #-} (MonadIO (t f)) => MonadIO (Via1 MonadIO t f)