{-# LANGUAGE UndecidableInstances #-}

{- | Traits are optional attributes associated with a value. For
 example, a list containing totally ordered values might have a
 @Maximum@ trait where the associated attribute is the maximum
 value. This trait exists only if the list is non-empty. The `Trait`
 typeclass provides an interface to extract such trait attributes.

 Traits help to link attributes with values 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.Core.Trait (
  -- * Core Types
  Trait (..),
  TraitAbsence (..),
  Get (..),
  Gets,
  Linked,
  Set (..),
  Sets,

  -- * Linking values with attributes
  linkzero,
  linkminus,
  unlink,
  probe,
  plant,

  -- * Retrive trait attributes from linked values
  HasTrait (..),
  HaveTraits,
  pick,
  MissingTrait,
) where

import Control.Arrow (Arrow (..))
import Data.Kind (Constraint, Type)
import Data.Tagged (Tagged (..), untag)
import GHC.TypeLits (ErrorMessage (..), TypeError)

-- | A trait is an attribute @t@ associated with a value @a@.
class Trait (t :: Type) a where
  -- | Type of the associated attribute when the trait holds for a
  -- value
  type Attribute t a :: Type

-- | A trait @t@ that can be retrieved from @a@ but could be absent.
class Trait t a => TraitAbsence t a where
  -- | Type that indicates that the trait does not exist for a
  -- value. This could be an error message, exception etc.
  type Absence t a :: Type

-- | Extract trait attributes from a value.
class (Arrow h, TraitAbsence t a) => Get h t a where
  -- | Attempt to deduce the trait attribute from the value @a@.
  getTrait ::
    -- | The trait to extract
    t ->
    -- | Arrow that extracts the trait and can possibly fail
    h (Linked ts a) (Either (Absence t a) (Attribute t a))

-- | Set a trait attribute on a value
class (Arrow h, Trait t a) => Set h (t :: Type) a where
  -- | Set a trait attribute @t@ on the value @a@.
  setTrait ::
    -- | The trait to set
    t ->
    -- | A function to generate a linked value. This function must be
    -- called by the `setTrait` implementation to generate a linked
    -- value.
    (Linked ts a -> a -> Attribute t a -> Linked (t : ts) a) ->
    -- | An arrow that attches a new trait attribute to a value linked
    -- with other traits
    h (Linked ts a, Attribute t a) (Linked (t : ts) a)

-- | @Gets h ts a@ is equivalent to @(Get h t1 a, Get h t2 a, ..., Get
-- h tn a)@ where @ts = [t1, t2, ..., tn]@.
type family Gets h ts a :: Constraint where
  Gets h '[] a = ()
  Gets h (t : ts) a = (Get h t a, Gets h ts a)

-- | @Sets h ts a@ is equivalent to @(Set h t1 a, Set h t2 a, ..., Set
-- h tn a)@ where @ts = [t1, t2, ..., tn]@.
type family Sets h ts a :: Constraint where
  Sets h '[] a = ()
  Sets h (t : ts) a = (Set h t a, Sets h ts a)

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

type family LinkedAttributes (ts :: [Type]) (a :: Type) where
  LinkedAttributes '[] a = ()
  LinkedAttributes (t : ts) a = (Attribute t a, LinkedAttributes ts a)

-- | Wrap a value with an empty list of traits.
linkzero :: a -> Linked '[] a
linkzero :: forall a. a -> Linked '[] a
linkzero = forall (ts :: [*]) a. LinkedAttributes ts a -> a -> Linked ts a
Linked ()

-- | Forget the head trait
linkminus :: Linked (t : ts) a -> Linked ts a
linkminus :: forall t (ts :: [*]) a. Linked (t : ts) a -> Linked ts a
linkminus (Linked (Attribute t a
_, LinkedAttributes ts a
rv) a
a) = forall (ts :: [*]) a. LinkedAttributes ts a -> a -> Linked ts a
Linked LinkedAttributes ts a
rv a
a

{- | Attempt to link an additional trait with an already linked
 value. This can fail indicating an 'Absence' of the trait.
-}
probe ::
  forall t ts h a.
  Get h t a =>
  t ->
  h (Linked ts a) (Either (Absence t a) (Linked (t : ts) a))
probe :: forall t (ts :: [*]) (h :: * -> * -> *) a.
Get h t a =>
t -> h (Linked ts a) (Either (Absence t a) (Linked (t : ts) a))
probe t
t = proc Linked ts a
l -> do
  Either (Absence t a) (Attribute t a)
res <- forall (h :: * -> * -> *) t a (ts :: [*]).
Get h t a =>
t -> h (Linked ts a) (Either (Absence t a) (Attribute t a))
getTrait t
t -< Linked ts a
l
  forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall e.
(Linked ts a, Either e (Attribute t a))
-> Either e (Linked (t : ts) a)
link -< (Linked ts a
l, Either (Absence t a) (Attribute t a)
res)
  where
    link :: (Linked ts a, Either e (Attribute t a)) -> Either e (Linked (t : ts) a)
    link :: forall e.
(Linked ts a, Either e (Attribute t a))
-> Either e (Linked (t : ts) a)
link (Linked ts a
_, Left e
e) = forall a b. a -> Either a b
Left e
e
    link (Linked{a
LinkedAttributes ts a
unlink :: a
linkAttribute :: LinkedAttributes ts a
linkAttribute :: forall (ts :: [*]) a. Linked ts a -> LinkedAttributes ts a
unlink :: forall (ts :: [*]) a. Linked ts a -> a
..}, Right Attribute t a
attr) = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ Linked{linkAttribute :: LinkedAttributes (t : ts) a
linkAttribute = (Attribute t a
attr, LinkedAttributes ts a
linkAttribute), a
unlink :: a
unlink :: a
..}

-- | Set a trait attribute on linked value to produce another linked
-- value
plant :: forall t ts h a. Set h t a => t -> h (Linked ts a, Attribute t a) (Linked (t : ts) a)
plant :: forall t (ts :: [*]) (h :: * -> * -> *) a.
Set h t a =>
t -> h (Linked ts a, Attribute t a) (Linked (t : ts) a)
plant t
t = proc (Linked ts a
l, Attribute t a
attr) -> do
  forall (h :: * -> * -> *) t a (ts :: [*]).
Set h t a =>
t
-> (Linked ts a -> a -> Attribute t a -> Linked (t : ts) a)
-> h (Linked ts a, Attribute t a) (Linked (t : ts) a)
setTrait t
t Linked ts a -> a -> Attribute t a -> Linked (t : ts) a
link -< (Linked ts a
l, Attribute t a
attr)
  where
    link :: Linked ts a -> a -> Attribute t a -> Linked (t : ts) a
    link :: Linked ts a -> a -> Attribute t a -> Linked (t : ts) a
link Linked{a
LinkedAttributes ts a
unlink :: a
linkAttribute :: LinkedAttributes ts a
linkAttribute :: forall (ts :: [*]) a. Linked ts a -> LinkedAttributes ts a
unlink :: forall (ts :: [*]) a. Linked ts a -> a
..} a
a' Attribute t a
attr = Linked{linkAttribute :: LinkedAttributes (t : ts) a
linkAttribute = (Attribute t a
attr, LinkedAttributes ts a
linkAttribute), unlink :: a
unlink = a
a'}

{- | Constraint that proves that the trait @t@ is present in the list
 of traits @ts@.
-}
class HasTrait t ts where
  -- | Get the attribute associated with @t@ from a linked value. See also: 'pick'.
  from :: Linked ts a -> Tagged t (Attribute t a)

instance HasTrait t (t : ts) where
  from :: Linked (t : ts) a -> Tagged t (Attribute t a)
  from :: forall a. Linked (t : ts) a -> Tagged t (Attribute t a)
from (Linked (Attribute t a
lv, LinkedAttributes ts a
_) a
_) = forall {k} (s :: k) b. b -> Tagged s b
Tagged Attribute t a
lv

instance {-# OVERLAPPABLE #-} HasTrait t ts => HasTrait t (t' : ts) where
  from :: Linked (t' : ts) a -> Tagged t (Attribute t a)
  from :: forall a. Linked (t' : ts) a -> Tagged t (Attribute t a)
from Linked (t' : ts) a
l = forall t (ts :: [*]) a.
HasTrait t ts =>
Linked ts a -> Tagged t (Attribute t a)
from forall a b. (a -> b) -> a -> b
$ forall t (ts :: [*]) a. Linked (t : ts) a -> Linked ts a
linkminus Linked (t' : ts) a
l

{- | Retrieve a trait.

 @pick@ is used along with `from` to retrieve an attribute from a
 linked value:

 > pick @t $ from val
-}
pick :: Tagged t a -> a
pick :: forall {k} (t :: k) a. Tagged t a -> a
pick = forall {k} (t :: k) a. Tagged t a -> a
untag

-- For better type errors
instance TypeError (MissingTrait t) => HasTrait t '[] where
  from :: forall a. Linked '[] a -> Tagged t (Attribute t a)
from = forall a. HasCallStack => a
undefined

-- | Type error for nicer UX of missing traits
type MissingTrait t =
  Text "The request doesn't have the trait ‘" :<>: ShowType t :<>: Text "’."
    :$$: Text ""
    :$$: Text "Did you use a wrong trait type?"
    :$$: Text "For e.g., ‘QueryParam \"foo\" Int’ instead of ‘QueryParam \"foo\" String’?"
    :$$: Text ""
    :$$: Text "Or did you forget to apply an appropriate middleware?"
    :$$: Text "For e.g. The trait ‘JSONBody t’ can be used with ‘jsonRequestBody @t’ middleware."
    :$$: Text ""

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