{-# LANGUAGE UndecidableInstances #-}
-- |
-- Copyright        : (c) Raghu Kaippully, 2020
-- License          : MPL-2.0
-- Maintainer       : rkaippully@gmail.com
--
-- Traits are optional attributes that a value might posess. For example,
-- a list containing totally ordered values might have a @Maximum@ trait
-- where the associated attribute is the maximum value. The trait exists
-- only if the list is non-empty.
--
-- Traits help to access these attributes in a type-safe manner.
--
-- Traits are somewhat similar to [refinement
-- types](https://hackage.haskell.org/package/refined), but allow
-- arbitrary attributes to be associated with a value instead of only a
-- predicate.
module WebGear.Trait
  ( -- * Core Types
    Trait (..)
  , CheckResult (..)
  , Linked
  , Traits

    -- * Linking values with traits
  , linkzero
  , linkplus
  , linkminus
  , unlink

    -- * Retrive trait attributes from linked values
  , Has (..)
  , Have
  ) where

import Data.Kind (Constraint, Type)
import Data.Tagged (Tagged (..))


-- | A 'Trait' is an optional attribute @t@ associated with a value @a@.
--
-- The 'check' function validates the presence of the trait for a
-- given value. Checking the presence of the trait can optionally
-- modify the value as well.
class Monad m => Trait t a m where
  -- | Type of the associated attribute
  type Val t a

  -- | Type of check failures
  type Fail t a

  -- | Checks the presence of the associated attribute.
  check :: a -> m (CheckResult t a)

-- | Result of a 'check' operation
data CheckResult t a = CheckSuccess a (Val t a)
                     | CheckFail (Fail t a)

deriving instance (Eq a, Eq (Val t a), Eq (Fail t a)) => Eq (CheckResult t a)
deriving instance (Show a, Show (Val t a), Show (Fail t a)) => Show (CheckResult t a)
deriving instance (Read a, Read (Val t a), Read (Fail t a)) => Read (CheckResult t a)


-- | A trivial trait that is always present and whose attribute does
-- not carry any meaningful information.
instance Monad m => Trait '[] a m where
  type Val '[] a = ()
  type Fail '[] a = ()

  check :: a -> m (CheckResult '[] a)
  check :: a -> m (CheckResult '[] a)
check a :: a
a = CheckResult '[] a -> m (CheckResult '[] a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckResult '[] a -> m (CheckResult '[] a))
-> CheckResult '[] a -> m (CheckResult '[] a)
forall a b. (a -> b) -> a -> b
$ a -> Val '[] a -> CheckResult '[] a
forall k (t :: k) a. a -> Val t a -> CheckResult t a
CheckSuccess a
a ()

-- | Combination of many traits all of which are present for a value.
instance (Trait t a m, Trait ts a m) => Trait (t:ts) a m where
  type Val (t:ts) a = (Val t a, Val ts a)
  type Fail (t:ts) a = Either (CheckResult t a) (CheckResult ts a)

  check :: a -> m (CheckResult (t:ts) a)
  check :: a -> m (CheckResult (t : ts) a)
check a :: a
a = a -> m (CheckResult t a)
forall k (t :: k) a (m :: * -> *).
Trait t a m =>
a -> m (CheckResult t a)
check @t a
a m (CheckResult t a)
-> (CheckResult t a -> m (CheckResult (t : ts) a))
-> m (CheckResult (t : ts) a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    e :: CheckResult t a
e@(CheckFail _)   -> CheckResult (t : ts) a -> m (CheckResult (t : ts) a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckResult (t : ts) a -> m (CheckResult (t : ts) a))
-> CheckResult (t : ts) a -> m (CheckResult (t : ts) a)
forall a b. (a -> b) -> a -> b
$ Fail (t : ts) a -> CheckResult (t : ts) a
forall k (t :: k) a. Fail t a -> CheckResult t a
CheckFail (Fail (t : ts) a -> CheckResult (t : ts) a)
-> Fail (t : ts) a -> CheckResult (t : ts) a
forall a b. (a -> b) -> a -> b
$ CheckResult t a -> Either (CheckResult t a) (CheckResult ts a)
forall a b. a -> Either a b
Left CheckResult t a
e
    CheckSuccess a' :: a
a' l :: Val t a
l -> a -> m (CheckResult ts a)
forall k (t :: k) a (m :: * -> *).
Trait t a m =>
a -> m (CheckResult t a)
check @ts a
a' m (CheckResult ts a)
-> (CheckResult ts a -> m (CheckResult (t : ts) a))
-> m (CheckResult (t : ts) a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      e :: CheckResult ts a
e@(CheckFail _)    -> CheckResult (t : ts) a -> m (CheckResult (t : ts) a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckResult (t : ts) a -> m (CheckResult (t : ts) a))
-> CheckResult (t : ts) a -> m (CheckResult (t : ts) a)
forall a b. (a -> b) -> a -> b
$ Fail (t : ts) a -> CheckResult (t : ts) a
forall k (t :: k) a. Fail t a -> CheckResult t a
CheckFail (Fail (t : ts) a -> CheckResult (t : ts) a)
-> Fail (t : ts) a -> CheckResult (t : ts) a
forall a b. (a -> b) -> a -> b
$ CheckResult ts a -> Either (CheckResult t a) (CheckResult ts a)
forall a b. b -> Either a b
Right CheckResult ts a
e
      CheckSuccess a'' :: a
a'' r :: Val ts a
r -> CheckResult (t : ts) a -> m (CheckResult (t : ts) a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CheckResult (t : ts) a -> m (CheckResult (t : ts) a))
-> CheckResult (t : ts) a -> m (CheckResult (t : ts) a)
forall a b. (a -> b) -> a -> b
$ a -> Val (t : ts) a -> CheckResult (t : ts) a
forall k (t :: k) a. a -> Val t a -> CheckResult t a
CheckSuccess a
a'' (Val t a
l, Val ts a
r)

-- | Constraint for functions that use multiple traits
type family Traits ts a m :: Constraint where
  Traits '[]    a m = ()
  Traits (t:ts) a m = (Trait t a m, Traits ts a m)

-- | A value linked with a type-level list of traits.
data Linked (ts :: [Type]) a = Linked
    { Linked ts a -> Val ts a
linkVal :: !(Val ts a)
    , Linked ts a -> a
unlink  :: !a           -- ^ Retrive the value from a linked value
    }

-- | Link a value with the trivial trait
linkzero :: a -> Linked '[] a
linkzero :: a -> Linked '[] a
linkzero = Val '[] a -> a -> Linked '[] a
forall (ts :: [*]) a. Val ts a -> a -> Linked ts a
Linked ()

-- | Attempt to link an additional trait with an already linked value
linkplus :: Trait t a m => Linked ts a -> m (Either (Fail t a) (Linked (t:ts) a))
linkplus :: Linked ts a -> m (Either (Fail t a) (Linked (t : ts) a))
linkplus l :: Linked ts a
l = do
  CheckResult t a
v <- a -> m (CheckResult t a)
forall k (t :: k) a (m :: * -> *).
Trait t a m =>
a -> m (CheckResult t a)
check (Linked ts a -> a
forall (ts :: [*]) a. Linked ts a -> a
unlink Linked ts a
l)
  pure $ CheckResult t a
-> Linked ts a -> Either (Fail t a) (Linked (t : ts) a)
forall t a (ts :: [*]).
CheckResult t a
-> Linked ts a -> Either (Fail t a) (Linked (t : ts) a)
mkLinked CheckResult t a
v Linked ts a
l
  where
    mkLinked :: CheckResult t a -> Linked ts a -> Either (Fail t a) (Linked (t:ts) a)
    mkLinked :: CheckResult t a
-> Linked ts a -> Either (Fail t a) (Linked (t : ts) a)
mkLinked (CheckSuccess a :: a
a left :: Val t a
left) lv :: Linked ts a
lv = Linked (t : ts) a -> Either (Fail t a) (Linked (t : ts) a)
forall a b. b -> Either a b
Right (Linked (t : ts) a -> Either (Fail t a) (Linked (t : ts) a))
-> Linked (t : ts) a -> Either (Fail t a) (Linked (t : ts) a)
forall a b. (a -> b) -> a -> b
$ Val (t : ts) a -> a -> Linked (t : ts) a
forall (ts :: [*]) a. Val ts a -> a -> Linked ts a
Linked (Val t a
left, Linked ts a -> Val ts a
forall (ts :: [*]) a. Linked ts a -> Val ts a
linkVal Linked ts a
lv) a
a
    mkLinked (CheckFail e :: Fail t a
e) _          = Fail t a -> Either (Fail t a) (Linked (t : ts) a)
forall a b. a -> Either a b
Left Fail t a
e

-- | Remove the leading trait from the linked value
linkminus :: Linked (t:ts) a -> Linked ts a
linkminus :: Linked (t : ts) a -> Linked ts a
linkminus l :: Linked (t : ts) a
l = Val ts a -> a -> Linked ts a
forall (ts :: [*]) a. Val ts a -> a -> Linked ts a
Linked ((Val t a, Val ts a) -> Val ts a
forall a b. (a, b) -> b
snd ((Val t a, Val ts a) -> Val ts a)
-> (Val t a, Val ts a) -> Val ts a
forall a b. (a -> b) -> a -> b
$ Linked (t : ts) a -> Val (t : ts) a
forall (ts :: [*]) a. Linked ts a -> Val ts a
linkVal Linked (t : ts) a
l) (Linked (t : ts) a -> a
forall (ts :: [*]) a. Linked ts a -> a
unlink Linked (t : ts) a
l)


-- | Constraint that proves that the trait @t@ is present somewhere in
-- the list of traits @ts@.
class Has t ts where
  traitValue :: Linked ts a -> Tagged t (Val t a)

instance Has t (t:ts) where
  traitValue :: Linked (t : ts) a -> Tagged t (Val t a)
  traitValue :: Linked (t : ts) a -> Tagged t (Val t a)
traitValue (Linked (lv, _) _) = Val t a -> Tagged t (Val t a)
forall k (s :: k) b. b -> Tagged s b
Tagged Val t a
lv

instance {-# OVERLAPPABLE #-} Has t ts => Has t (t':ts) where
  traitValue :: Linked (t':ts) a -> Tagged t (Val t a)
  traitValue :: Linked (t' : ts) a -> Tagged t (Val t a)
traitValue l :: Linked (t' : ts) a
l = Linked ts a -> Tagged t (Val t a)
forall k (t :: k) (ts :: [*]) a.
Has t ts =>
Linked ts a -> Tagged t (Val t a)
traitValue (Linked (t' : ts) a -> Linked ts a
forall q (qs :: [*]) b. Linked (q : qs) b -> Linked qs b
rightLinked Linked (t' : ts) a
l)
    where
      rightLinked :: Linked (q:qs) b -> Linked qs b
      rightLinked :: Linked (q : qs) b -> Linked qs b
rightLinked (Linked (_, rv) a :: b
a) = Val qs b -> b -> Linked qs b
forall (ts :: [*]) a. Val ts a -> a -> Linked ts a
Linked Val qs b
rv b
a


-- | Constraint that proves that all the traits in the list @ts@ are
-- present in the list @qs@.
type family Have ts qs :: Constraint where
  Have '[]    qs = ()
  Have (t:ts) qs = (Has t qs, Have ts qs)