content: -- |
  -- Module      :  Data.Refined
  -- Copyright   :  © 2018 Mark Karpov
  -- License     :  BSD 3 clause
  --
  -- Maintainer  :  Mark Karpov <markkarpov92@gmail.com>
  -- Stability   :  experimental
  -- Portability :  portable
  --
  -- The module introduces a framework that allows us to manipulate refined
  -- types. The documentation is meant to be read as an article from top to
  -- bottom, as it serves as a manual and gradually introduces various
  -- features of the library.
  
  {-# LANGUAGE AllowAmbiguousTypes    #-}
  {-# LANGUAGE DataKinds              #-}
  {-# LANGUAGE DeriveDataTypeable     #-}
  {-# LANGUAGE DeriveGeneric          #-}
  {-# LANGUAGE FlexibleContexts       #-}
  {-# LANGUAGE FlexibleInstances      #-}
  {-# LANGUAGE FunctionalDependencies #-}
  {-# LANGUAGE MultiParamTypeClasses  #-}
  {-# LANGUAGE PolyKinds              #-}
  {-# LANGUAGE RecordWildCards        #-}
  {-# LANGUAGE RoleAnnotations        #-}
  {-# LANGUAGE ScopedTypeVariables    #-}
  {-# LANGUAGE TemplateHaskell        #-}
  {-# LANGUAGE TypeApplications       #-}
  {-# LANGUAGE TypeFamilies           #-}
  {-# LANGUAGE TypeOperators          #-}
  {-# LANGUAGE UndecidableInstances   #-}
  
  module Data.Refined
    ( -- * 'Refined' types
      Refined
    , refined
    , unrefined
      -- * 'Prop'erties
    , Prop (..)
    , IdProp
    , PropName
    , AddProp
    , HasProp
    , HasProps
    , ProjectionProps
      -- * Establishing properties
    , assumeProp
    , estPropThrow
    , estPropFail
    , estPropError
    , estPropTH
    , RefinedException (..)
      -- * Following properties
    , Via
    , followProp
      -- * Deducing properties
    , Axiom
    , V
    , applyAxiom
    , selectProps )
  where
  
  import Control.Monad
  import Control.Monad.Catch (Exception (..), MonadThrow (..))
  import Control.Monad.Except (MonadError (..))
  import Data.Coerce
  import Data.Kind
  import Data.Proxy
  import Data.Typeable (Typeable)
  import GHC.Generics
  import GHC.Stack
  import GHC.TypeLits
  import qualified Control.Monad.Fail         as Fail
  import qualified Language.Haskell.TH.Syntax as TH
  
  ----------------------------------------------------------------------------
  -- Refined types
  
  -- | @'Refined' ps a@ is a wrapper around @a@ proving that it has properties
  -- @ps@. @ps@ is a type-level list containing /properties/, that is, void
  -- data types symbolizing various concepts, see 'Prop'.
  
  newtype Refined (ps :: [*]) a = Refined a
    deriving (Eq, Ord, Show, Typeable)
  
  type role Refined phantom nominal
  
  instance TH.Lift a => TH.Lift (Refined ps a) where
    lift (Refined a) = [| Refined a |]
  
  -- | 'refined' creates a refined type with no associated properties. We
  -- don't demand anything, and so quite conveniently this is a pure function.
  
  refined :: a -> Refined '[] a
  refined = Refined
  
  -- | We can erase information we know by using 'unrefined'.
  
  unrefined :: Refined ps a -> a
  unrefined (Refined a) = a
  
  ----------------------------------------------------------------------------
  -- Properties
  
  -- | @'Prop' a p@ is a type class for @a@ things that can have @p@ property.
  -- Properties are morphisms in the category of refined types. (That category
  -- is the Kleisli category of the @'Either' 'String'@ monad as it seems to
  -- happen here.)
  
  class (Show a, Generic p) => Prop a p where
  
    -- | If we consider property @p@ as a morphism, then while @a@ is its
    -- domain, @'PropProjection' a p@ is the codomain.
    --
    -- We could have a property telling that a @Text@ value is not empty,
    -- then:
    --
    -- > type PropProjection Text NotEmpty = NonEmptyText -- e.g. a newtype
    --
    -- We could do the same for linked lists:
    --
    -- > type PropProjection [Char] NotEmpty = NonEmpty Char
    --
    -- This connects the 'Data.List.NonEmpty.NonEmpty' type, normally
    -- obtainable via the smart constructor 'Data.List.NonEmpty.nonEmpty' to
    -- our list. Once we have proven that our list is @NotEmpty@, we'll be
    -- able to get @NonEmpty@ projection purely without possibility of
    -- failure.
    --
    -- We could have a property called @Length@ and in that case we could say:
    --
    -- > type PropProjection Text Length = Int
    --
    -- We could also have a property @IsURI@ telling if a @Text@ value is a
    -- valid @URI@. In that case we could say (assuming that @URI@ is such a
    -- type that can represent only valid URIs):
    --
    -- > type PropProjection Text IsURI = URI
  
    type PropProjection a p :: *
  
    -- | 'checkProp' is the way to check if @a@ has property @p@. It either
    -- has it, and then we obtain @'PropProjection' a p@ or it doesn't have
    -- such a property, in which case a reason “why” is returned as a
    -- 'String'.
  
    checkProp :: Proxy p -> a -> Either String (PropProjection a p)
  
  -- | Identity property. This is the identity in the category of refined
  -- types.
  
  data IdProp deriving Generic
  
  -- | Every type has the identity property which allows us to treat that type
  -- as well… that type.
  
  instance Show a => Prop a IdProp where
    type PropProjection a IdProp = a
    checkProp Proxy = Right
  
  -- | We always can assume that a value has 'IdProp'.
  
  instance Axiom "id_prop" '[] '[] IdProp
  
  -- | An existing property can be pre-composed with 'IdProp'.
  
  instance Axiom "id_prop_pre" '[a] '[a] (a `Via` IdProp)
  
  -- | Pre-composition of 'IdProp' can be dropped.
  
  instance Axiom "id_prop_pre'" '[a] '[a `Via` IdProp] a
  
  -- | An existing prperty can be post-composed with 'IdProp'.
  
  instance Axiom "id_prop_post" '[a] '[a] (IdProp `Via` a)
  
  -- | Post-composition of 'IdProp' can be dropped.
  
  instance Axiom "id_prop_post'" '[a] '[IdProp `Via` a] a
  
  -- | Obtain a name of property type as a type of the kind 'Symbol'.
  
  type family PropName (p :: *) :: Symbol where
    PropName (a `Via` b) = "*"
      `AppendSymbol` PropName' (Rep a)
      `AppendSymbol` "*via*"
      `AppendSymbol` PropName' (Rep b)
    PropName p = PropName' (Rep p)
  
  -- | A helper for 'PropName'.
  
  type family PropName' (p :: * -> *) :: Symbol where
    PropName' (D1 ('MetaData n m p nt) V1) =
      p `AppendSymbol` "-" `AppendSymbol` m `AppendSymbol` "-" `AppendSymbol` n
    PropName' p = TypeError
      ('Text "Types that represent properties should not have data constructors")
  
  -- | Add a property @p@ to the type-level set @ps@. If a property is already
  -- in the set, nothing will happen. The order of items in the set is
  -- (mostly) deterministic.
  
  type family AddProp (ps :: [*]) (p :: *) :: [*] where
    AddProp '[] p = '[p]
    AddProp (n ': ps) p = AddPropC (CmpSymbol (PropName p) (PropName n)) p n ps
  
  type family AddPropC (o :: Ordering) (a :: *) (b :: *) (as :: [*]) :: [*] where
    AddPropC 'LT a b as = a ': b ': as
    AddPropC 'EQ a a as = a ': as
    AddPropC 'EQ a b as = a ': b ': as
    AddPropC 'GT a b as = b ': AddProp as a
  
  -- | The resulting constraint will be satisfied iff the collection of
  -- properties @ps@ has the property @p@ is it.
  
  type family HasProp (ps :: [*]) (p :: *) :: Constraint where
    HasProp '[] p = TypeError
      ('ShowType p ':<>: 'Text " is not a proven property")
    HasProp (p ': ps) p = ()
    HasProp (b ': ps) p = HasProp ps p
  
  -- | Like 'HasProp' but for many properties at once.
  
  type family HasProps (ps :: [*]) (qs :: [*]) :: Constraint where
    HasProps ps '[] = ()
    HasProps ps (q ': qs) = (HasProp ps q, HasProps ps qs)
  
  -- | Construct a list of properties from @ps@ for projection obtained via
  -- @p@.
  
  type family ProjectionProps (ps :: [*]) (p :: *)  :: [*] where
    ProjectionProps ps (t `Via` p) = ProjectionProps (ProjectionProps ps p) t
    ProjectionProps '[] p = '[]
    ProjectionProps ((t `Via` p) ': ps) p = t ': ProjectionProps ps p
    ProjectionProps (x ': ps) p = ProjectionProps ps p
  
  ----------------------------------------------------------------------------
  -- Establishing properties
  
  -- | Assume a property. This is unsafe and may be a source of bugs. Only use
  -- when you 100% sure that the property indeed holds.
  
  assumeProp
    :: forall q ps a. (Prop a q)
    => Refined ps a
    -> Refined (ps `AddProp` q) a
  assumeProp = coerce
  
  -- | Establish a property in a 'MonadThrow' instance.
  
  estPropThrow
    :: forall q ps m a. ( Prop a q
                        , KnownSymbol (PropName q)
                        , MonadThrow m
                        )
    => Refined ps a
    -> m (Refined (ps `AddProp` q) a)
  estPropThrow = either throwM return . probeProp @q
  
  -- | Establish a property in a 'Fail.MonadFail' instance.
  
  estPropFail
    :: forall q ps m a. ( Prop a q
                        , KnownSymbol (PropName q)
                        , Fail.MonadFail m
                        )
    => Refined ps a
    -> m (Refined (ps `AddProp` q) a)
  estPropFail = either (Fail.fail . displayException) return . probeProp @q
  
  -- | Establish a property in a 'MonadError' instance.
  
  estPropError
    :: forall q ps m a. ( Prop a q
                        , KnownSymbol (PropName q)
                        , MonadError RefinedException m
                        )
    => Refined ps a
    -> m (Refined (ps `AddProp` q) a)
  estPropError = either throwError return . probeProp @q
  
  -- | Establish a property at compile time using Template Haskell.
  
  estPropTH
    :: forall q ps a. ( Prop a q
                      , KnownSymbol (PropName q)
                      , TH.Lift a
                      )
    => Refined ps a
    -> TH.Q TH.Exp
  estPropTH x = estPropFail @q x >>= TH.lift
  
  -- | Check if a property holds and return error message if it doesn't.
  
  probeProp
    :: forall q ps a. ( Prop a q
                      , KnownSymbol (PropName q)
                      , HasCallStack
                      )
    => Refined ps a
    -> Either RefinedException (Refined (ps `AddProp` q) a)
  probeProp (Refined a) =
    case checkProp (Proxy :: Proxy q) a of
      Left issue -> Left RefinedException
        { rexpCallStack = callStack
        , rexpValue = show a
        , rexpPropName = symbolVal (Proxy :: Proxy (PropName q))
        , rexpIssue = issue
        }
      Right _ -> Right (Refined a)
  
  -- | Exception that is thrown at run time when a property doesn't hold.
  
  data RefinedException = RefinedException
    { rexpCallStack :: !CallStack
      -- ^ Location where the check failed
    , rexpValue :: !String
      -- ^ Value that failed to satisfy a property check
    , rexpPropName :: !String
      -- ^ Name of the property in question
    , rexpIssue :: !String
      -- ^ Description of why the property check failed
    } deriving (Show, Typeable)
  
  instance Exception RefinedException where
    displayException RefinedException {..} = unlines
      [ "RefinedException:"
      , prettyCallStack rexpCallStack
      , "value: " ++ rexpValue
      , "property: " ++ rexpPropName
      , "issue:" ++ rexpIssue
      ]
  
  ----------------------------------------------------------------------------
  -- Following properties
  
  -- | 'Via' is the composition in the category of refined types.
  --
  -- 'Via' is of great utility as it allows us to prove properties about
  -- values of refined types that are obtainable by following a property
  -- morphism, not just values we currently have.
  --
  -- For example, having a @'Refined' '[] Text@ value we could demand that it
  -- has the property @GreaterThan 5 'Via' Length@:
  --
  -- > rText0 :: Refined '[] Text
  -- > rText0 = refined "foobar"
  -- >
  -- > -- In real programs use 'estMonadThrow' or similar, don't just blindly
  -- > -- assume things!
  -- > rText1 :: Refined '[GreaterThan 5 `Via` Length]
  -- > rText1 = assumeProp @(GreaterThan 5 `Via` Length) rText0
  --
  -- Then we could “follow” the @Length@ property with 'followProp' (see
  -- below) to get @Refined '[GreaterThan 5] Int@:
  --
  -- > rLength :: Refined '[GreaterThan 5] Int
  -- > rLength = followProp @Length rText1
  --
  -- It also allows us to state 'Axiom's (see below) that talk about
  -- properties of “connected” types. Without 'Via', 'Axiom's could only talk
  -- about relations between properties of the same type.
  
  data (t :: *) `Via` (p :: *) deriving Generic
  
  instance (Prop (PropProjection a p) t, Prop a p) => Prop a (t `Via` p) where
  
    type PropProjection a (t `Via` p) = PropProjection (PropProjection a p) t
  
    checkProp Proxy =
      checkProp (Proxy :: Proxy p) >=> checkProp (Proxy :: Proxy t)
  
  infixl 5 `Via`
  
  -- | Obtain a projection as a refined value, i.e. follow a morphism created
  -- by a property.
  
  followProp :: forall p ps a. (Prop a p, ps `HasProp` p, HasCallStack)
    => Refined ps a
    -> Refined (ProjectionProps ps p) (PropProjection a p)
  followProp (Refined a) =
    case checkProp (Proxy :: Proxy p) a of
      Left msg -> error $
        prettyCallStack callStack ++ "\n" ++
        show a ++ ": " ++ msg
      Right x -> Refined x
  
  ----------------------------------------------------------------------------
  -- Deducing properties
  
  -- | An @'Axiom' name vs qs p@ allows us to prove property @p@ if properties
  -- @qs@ are already proven. @name@ and arguments @vs@ determine both @qs@
  -- and @p@.
  --
  -- The arguments are necessary sometimes. Imagine you want to write
  -- something as trivial as:
  --
  -- > instance CmpNat n m ~ GT => Axiom "weaken_gt"
  -- >     '[V n, V m] '[GreaterThan n] (GreaterThan m)
  --
  -- Without having @vs@ you'd have a hard time convincing GHC that this could
  -- work.
  --
  -- Another example. Suppose I have two refined types @A@ and @B@ and
  -- properties @PropM@ and @PropN@ such that @PropM@ allows me to go from @A@
  -- to @B@ and @PropN@ allows me to go back to get exactly the same value of
  -- @A@ as before. Now it makes sense that I could arrange things is such a
  -- way that when I'm “back” I can recover any properties that I originally
  -- knew about @A@.
  --
  -- > instance Axiom "preserve" '[p] '[p] (p `Via` PropN `Via` PropM)
  --
  -- Now I can first create as many properties as necessary of the form @p
  -- `Via` PropN `Via` PropM@, then use @PropM@ to go to @B@ with help of
  -- 'followProp'. After that I'll be able to go back to @A@ and my old
  -- properties “preserved” in that way will be with me.
  --
  -- Again, without the argument parameter @vs@ that trick would be
  -- impossible.
  
  class Axiom (name :: Symbol) (vs :: [*]) (qs :: [*]) (p :: *) | name vs -> qs p
  
  -- | A helper wrapper to help us construct heterogeneous type-level lists
  -- with respect to kinds of elements.
  
  data V (a :: k)
  
  -- | Apply 'Axiom' and deduce a new property.
  
  applyAxiom
    :: forall name vs p qs ps a. (Prop a p, Axiom name vs qs p, ps `HasProps` qs)
    => Refined ps a
    -> Refined (ps `AddProp` p) a
  applyAxiom = coerce
  
  -- | Select some properties from known properties.
  
  selectProps :: forall qs ps a. (ps `HasProps` qs)
    => Refined ps a
    -> Refined qs a
  selectProps = coerce
  