Copyright | © 2018 Mark Karpov |
---|---|
License | BSD 3 clause |
Maintainer | Mark Karpov <markkarpov92@gmail.com> |
Stability | experimental |
Portability | portable |
Safe Haskell | None |
Language | Haskell2010 |
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.
- data Refined (ps :: [*]) a
- refined :: a -> Refined '[] a
- unrefined :: Refined ps a -> a
- class (Show a, Generic p) => Prop a p where
- type PropProjection a p :: *
- data IdProp
- type family PropName (p :: *) :: Symbol where ...
- type family AddProp (ps :: [*]) (p :: *) :: [*] where ...
- type family HasProp (ps :: [*]) (p :: *) :: Constraint where ...
- type family HasProps (ps :: [*]) (qs :: [*]) :: Constraint where ...
- type family ProjectionProps (ps :: [*]) (p :: *) :: [*] where ...
- assumeProp :: forall q ps a. Prop a q => Refined ps a -> Refined (ps `AddProp` q) a
- estPropThrow :: forall q ps m a. (Prop a q, KnownSymbol (PropName q), MonadThrow m) => Refined ps a -> m (Refined (ps `AddProp` q) a)
- estPropFail :: forall q ps m a. (Prop a q, KnownSymbol (PropName q), MonadFail m) => Refined ps a -> m (Refined (ps `AddProp` q) a)
- estPropError :: forall q ps m a. (Prop a q, KnownSymbol (PropName q), MonadError RefinedException m) => Refined ps a -> m (Refined (ps `AddProp` q) a)
- estPropTH :: forall q ps a. (Prop a q, KnownSymbol (PropName q), Lift a) => Refined ps a -> Q Exp
- data RefinedException = RefinedException {
- rexpCallStack :: !CallStack
- rexpValue :: !String
- rexpPropName :: !String
- rexpIssue :: !String
- data Via (t :: *) (p :: *)
- followProp :: forall p ps a. (Prop a p, ps `HasProp` p, HasCallStack) => Refined ps a -> Refined (ProjectionProps ps p) (PropProjection a p)
- class Axiom (name :: Symbol) (vs :: [*]) (qs :: [*]) (p :: *) | name vs -> qs p
- data V (a :: k)
- 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
- selectProps :: forall qs ps a. ps `HasProps` qs => Refined ps a -> Refined qs a
Refined
types
refined :: a -> Refined '[] a Source #
refined
creates a refined type with no associated properties. We
don't demand anything, and so quite conveniently this is a pure function.
Prop
erties
class (Show a, Generic p) => Prop a p where Source #
is a type class for Prop
a pa
things that can have p
property.
Properties are morphisms in the category of refined types. (That category
is the Kleisli category of the
monad as it seems to
happen here.)Either
String
type PropProjection a p :: * Source #
If we consider property p
as a morphism, then while a
is its
domain,
is the codomain.PropProjection
a p
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 NonEmpty
type, normally
obtainable via the smart constructor 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
checkProp :: Proxy p -> a -> Either String (PropProjection a p) Source #
checkProp
is the way to check if a
has property p
. It either
has it, and then we obtain
or it doesn't have
such a property, in which case a reason “why” is returned as a
PropProjection
a pString
.
Identity property. This is the identity in the category of refined types.
Generic IdProp Source # | |
Show a => Prop a IdProp Source # | Every type has the identity property which allows to treat that type as well… that type. |
Axiom "id_prop" ([] *) ([] *) IdProp Source # | We always can assume that a value has |
Axiom "id_prop_post'" ((:) * a ([] *)) ((:) * (Via IdProp a) ([] *)) a Source # | Post-composition of |
Axiom "id_prop_pre'" ((:) * a ([] *)) ((:) * (Via a IdProp) ([] *)) a Source # | Pre-composition of |
Axiom "id_prop_post" ((:) * a ([] *)) ((:) * a ([] *)) (Via IdProp a) Source # | An existing prperty can be post-composed with |
Axiom "id_prop_pre" ((:) * a ([] *)) ((:) * a ([] *)) (Via a IdProp) Source # | An existing property can be pre-composed with |
type Rep IdProp Source # | |
type PropProjection a IdProp Source # | |
type family PropName (p :: *) :: Symbol where ... Source #
Obtain a name of property type as a type of the kind Symbol
.
PropName (a `Via` b) = (("*" `AppendSymbol` PropName' (Rep a)) `AppendSymbol` "*via*") `AppendSymbol` PropName' (Rep b) | |
PropName p = PropName' (Rep p) |
type family AddProp (ps :: [*]) (p :: *) :: [*] where ... Source #
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 HasProp (ps :: [*]) (p :: *) :: Constraint where ... Source #
The resulting constraint will be satisfied iff the collection of
properties ps
has the property p
is it.
type family HasProps (ps :: [*]) (qs :: [*]) :: Constraint where ... Source #
Like HasProp
but for many properties at once.
type family ProjectionProps (ps :: [*]) (p :: *) :: [*] where ... Source #
Construct a list of properties from ps
for projection obtained via
p
.
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
assumeProp :: forall q ps a. Prop a q => Refined ps a -> Refined (ps `AddProp` q) a Source #
Assume a property. This is unsafe and may be a source of bugs. Only use when you 100% sure that the property indeed holds.
estPropThrow :: forall q ps m a. (Prop a q, KnownSymbol (PropName q), MonadThrow m) => Refined ps a -> m (Refined (ps `AddProp` q) a) Source #
Establish a property in a MonadThrow
instance.
estPropFail :: forall q ps m a. (Prop a q, KnownSymbol (PropName q), MonadFail m) => Refined ps a -> m (Refined (ps `AddProp` q) a) Source #
Establish a property in a MonadFail
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) Source #
Establish a property in a MonadError
instance.
estPropTH :: forall q ps a. (Prop a q, KnownSymbol (PropName q), Lift a) => Refined ps a -> Q Exp Source #
Establish a property at compile time using Template Haskell.
data RefinedException Source #
Exception that is thrown at run time when a property doesn't hold.
RefinedException | |
|
Following properties
data Via (t :: *) (p :: *) infixl 5 Source #
Via
is the composition in the category of refined types.
Via
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
value we could demand that it
has the property Refined
'[] TextGreaterThan 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 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.
(Prop (PropProjection a p) t, Prop a p) => Prop a (Via t p) Source # | |
Axiom "id_prop_post'" ((:) * a ([] *)) ((:) * (Via IdProp a) ([] *)) a Source # | Post-composition of |
Axiom "id_prop_pre'" ((:) * a ([] *)) ((:) * (Via a IdProp) ([] *)) a Source # | Pre-composition of |
Axiom "id_prop_post" ((:) * a ([] *)) ((:) * a ([] *)) (Via IdProp a) Source # | An existing prperty can be post-composed with |
Axiom "id_prop_pre" ((:) * a ([] *)) ((:) * a ([] *)) (Via a IdProp) Source # | An existing property can be pre-composed with |
Generic (Via t p) Source # | |
type PropProjection a (Via t p) Source # | |
type Rep (Via t p) Source # | |
followProp :: forall p ps a. (Prop a p, ps `HasProp` p, HasCallStack) => Refined ps a -> Refined (ProjectionProps ps p) (PropProjection a p) Source #
Obtain a projection as a refined value, i.e. follow a morphism created by a property.
Deducing properties
class Axiom (name :: Symbol) (vs :: [*]) (qs :: [*]) (p :: *) | name vs -> qs p Source #
An
allows to prove property Axiom
name vs qs pp
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
, then use Via
PropN Via
PropMPropM
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.
Axiom "id_prop" ([] *) ([] *) IdProp Source # | We always can assume that a value has |
Axiom "id_prop_post'" ((:) * a ([] *)) ((:) * (Via IdProp a) ([] *)) a Source # | Post-composition of |
Axiom "id_prop_pre'" ((:) * a ([] *)) ((:) * (Via a IdProp) ([] *)) a Source # | Pre-composition of |
Axiom "id_prop_post" ((:) * a ([] *)) ((:) * a ([] *)) (Via IdProp a) Source # | An existing prperty can be post-composed with |
Axiom "id_prop_pre" ((:) * a ([] *)) ((:) * a ([] *)) (Via a IdProp) Source # | An existing property can be pre-composed with |
A helper wrapper to help us construct heterogeneous type-level lists with respect to kinds of elements.
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 Source #
Apply Axiom
and deduce a new property.
selectProps :: forall qs ps a. ps `HasProps` qs => Refined ps a -> Refined qs a Source #
Select some properties from known properties.