-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Refined types
--   
--   Refined types.
@package facts
@version 0.0.1.0


-- | 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.
module Data.Refined

-- | <tt><a>Refined</a> ps a</tt> is a wrapper around <tt>a</tt> proving
--   that it has properties <tt>ps</tt>. <tt>ps</tt> is a type-level list
--   containing <i>properties</i>, that is, void data types symbolizing
--   various concepts, see <a>Prop</a>.
data Refined (ps :: [*]) a

-- | <a>refined</a> 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

-- | We can erase information we know by using <a>unrefined</a>.
unrefined :: Refined ps a -> a

-- | <tt><a>Prop</a> a p</tt> is a type class for <tt>a</tt> things that
--   can have <tt>p</tt> property. Properties are morphisms in the category
--   of refined types. (That category is the Kleisli category of the
--   <tt><a>Either</a> <a>String</a></tt> monad as it seems to happen
--   here.)
class (Show a, Generic p) => Prop a p where {
    type family PropProjection a p :: *;
}

-- | <a>checkProp</a> is the way to check if <tt>a</tt> has property
--   <tt>p</tt>. It either has it, and then we obtain
--   <tt><a>PropProjection</a> a p</tt> or it doesn't have such a property,
--   in which case a reason “why” is returned as a <a>String</a>.
checkProp :: Prop a p => Proxy p -> a -> Either String (PropProjection a p)

-- | Identity property. This is the identity in the category of refined
--   types.
data IdProp

-- | Obtain a name of property type as a type of the kind <a>Symbol</a>.

-- | Add a property <tt>p</tt> to the type-level set <tt>ps</tt>. If a
--   property is already in the set, nothing will happen. The order of
--   items in the set is (mostly) deterministic.

-- | The resulting constraint will be satisfied iff the collection of
--   properties <tt>ps</tt> has the property <tt>p</tt> is it.

-- | Like <a>HasProp</a> but for many properties at once.

-- | Construct a list of properties from <tt>ps</tt> for projection
--   obtained via <tt>p</tt>.

-- | 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

-- | Establish a property in a <a>MonadThrow</a> instance.
estPropThrow :: forall q ps m a. (Prop a q, KnownSymbol (PropName q), MonadThrow m) => Refined ps a -> m (Refined (ps `AddProp` q) a)

-- | Establish a property in a <a>MonadFail</a> instance.
estPropFail :: forall q ps m a. (Prop a q, KnownSymbol (PropName q), MonadFail m) => Refined ps a -> m (Refined (ps `AddProp` q) a)

-- | Establish a property in a <a>MonadError</a> 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)

-- | Establish a property at compile time using Template Haskell.
estPropTH :: forall q ps a. (Prop a q, KnownSymbol (PropName q), Lift a) => Refined ps a -> Q Exp

-- | Exception that is thrown at run time when a property doesn't hold.
data RefinedException
RefinedException :: !CallStack -> !String -> !String -> !String -> RefinedException

-- | Location where the check failed
[rexpCallStack] :: RefinedException -> !CallStack

-- | Value that failed to satisfy a property check
[rexpValue] :: RefinedException -> !String

-- | Name of the property in question
[rexpPropName] :: RefinedException -> !String

-- | Description of why the property check failed
[rexpIssue] :: RefinedException -> !String

-- | <a>Via</a> is the composition in the category of refined types.
--   
--   <a>Via</a> is of great utility as it allows 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 <tt><a>Refined</a> '[] Text</tt> value we could
--   demand that it has the property <tt>GreaterThan 5 <a>Via</a>
--   Length</tt>:
--   
--   <pre>
--   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
--   </pre>
--   
--   Then we could “follow” the <tt>Length</tt> property with
--   <a>followProp</a> (see below) to get <tt>Refined '[GreaterThan 5]
--   Int</tt>:
--   
--   <pre>
--   rLength :: Refined '[GreaterThan 5] Int
--   rLength = followProp @Length rText1
--   </pre>
--   
--   It also allows to state <a>Axiom</a>s (see below) that talk about
--   properties of “connected” types. Without <a>Via</a>, <a>Axiom</a>s
--   could only talk about relations between properties of the same type.
data (t :: *) `Via` (p :: *)

-- | 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)

-- | An <tt><a>Axiom</a> name vs qs p</tt> allows to prove property
--   <tt>p</tt> if properties <tt>qs</tt> are already proven. <tt>name</tt>
--   and arguments <tt>vs</tt> determine both <tt>qs</tt> and <tt>p</tt>.
--   
--   The arguments are necessary sometimes. Imagine you want to write
--   something as trivial as:
--   
--   <pre>
--   instance CmpNat n m ~ GT =&gt; Axiom "weaken_gt"
--       '[V n, V m] '[GreaterThan n] (GreaterThan m)
--   </pre>
--   
--   Without having <tt>vs</tt> you'd have a hard time convincing GHC that
--   this could work.
--   
--   Another example. Suppose I have two refined types <tt>A</tt> and
--   <tt>B</tt> and properties <tt>PropM</tt> and <tt>PropN</tt> such that
--   <tt>PropM</tt> allows me to go from <tt>A</tt> to <tt>B</tt> and
--   <tt>PropN</tt> allows me to go back to get exactly the same value of
--   <tt>A</tt> 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 <tt>A</tt>.
--   
--   <pre>
--   instance Axiom "preserve" '[p] '[p] (p `Via` PropN `Via` PropM)
--   </pre>
--   
--   Now I can first create as many properties as necessary of the form
--   <tt>p <a>Via</a> PropN <a>Via</a> PropM</tt>, then use <tt>PropM</tt>
--   to go to <tt>B</tt> with help of <a>followProp</a>. After that I'll be
--   able to go back to <tt>A</tt> and my old properties “preserved” in
--   that way will be with me.
--   
--   Again, without the argument parameter <tt>vs</tt> 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 <a>Axiom</a> 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

-- | Select some properties from known properties.
selectProps :: forall qs ps a. (ps `HasProps` qs) => Refined ps a -> Refined qs a
instance GHC.Generics.Generic (Data.Refined.Via t p)
instance GHC.Show.Show Data.Refined.RefinedException
instance GHC.Generics.Generic Data.Refined.IdProp
instance GHC.Show.Show a => GHC.Show.Show (Data.Refined.Refined ps a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.Refined.Refined ps a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Refined.Refined ps a)
instance Data.Refined.Axiom "id_prop" '[] '[] Data.Refined.IdProp
instance Data.Refined.Axiom "id_prop_pre" '[a] '[a] (Data.Refined.Via a Data.Refined.IdProp)
instance Data.Refined.Axiom "id_prop_pre'" '[a] '[Data.Refined.Via a Data.Refined.IdProp] a
instance Data.Refined.Axiom "id_prop_post" '[a] '[a] (Data.Refined.Via Data.Refined.IdProp a)
instance Data.Refined.Axiom "id_prop_post'" '[a] '[Data.Refined.Via Data.Refined.IdProp a] a
instance (Data.Refined.Prop (Data.Refined.PropProjection a p) t, Data.Refined.Prop a p) => Data.Refined.Prop a (Data.Refined.Via t p)
instance GHC.Exception.Exception Data.Refined.RefinedException
instance GHC.Show.Show a => Data.Refined.Prop a Data.Refined.IdProp
instance Language.Haskell.TH.Syntax.Lift a => Language.Haskell.TH.Syntax.Lift (Data.Refined.Refined ps a)
