{-# 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 = pure $ CheckSuccess 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 = check @t a >>= \case
    e@(CheckFail _)   -> pure $ CheckFail $ Left e
    CheckSuccess a' l -> check @ts a' >>= \case
      e@(CheckFail _)    -> pure $ CheckFail $ Right e
      CheckSuccess a'' r -> pure $ CheckSuccess a'' (l, 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
    { linkVal :: !(Val ts a)
    , unlink  :: !a           -- ^ Retrive the value from a linked value
    }

-- | Link a value with the trivial trait
linkzero :: a -> Linked '[] a
linkzero = 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 l = do
  v <- check (unlink l)
  pure $ mkLinked v l
  where
    mkLinked :: CheckResult t a -> Linked ts a -> Either (Fail t a) (Linked (t:ts) a)
    mkLinked (CheckSuccess a left) lv = Right $ Linked (left, linkVal lv) a
    mkLinked (CheckFail e) _          = Left e

-- | Remove the leading trait from the linked value
linkminus :: Linked (t:ts) a -> Linked ts a
linkminus l = Linked (snd $ linkVal l) (unlink 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 (lv, _) _) = Tagged lv

instance {-# OVERLAPPABLE #-} Has t ts => Has t (t':ts) where
  traitValue :: Linked (t':ts) a -> Tagged t (Val t a)
  traitValue l = traitValue (rightLinked l)
    where
      rightLinked :: Linked (q:qs) b -> Linked qs b
      rightLinked (Linked (_, rv) a) = Linked rv 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)