Data.Refined

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.

Refined types

data Refined (ps :: [*]) a

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.

Instances

Eq a => Eq (Refined ps a)

Methods

(==) :: Refined ps a -> Refined ps a -> Bool

(/=) :: Refined ps a -> Refined ps a -> Bool

Ord a => Ord (Refined ps a)

Methods

compare :: Refined ps a -> Refined ps a -> Ordering

(<) :: Refined ps a -> Refined ps a -> Bool

(<=) :: Refined ps a -> Refined ps a -> Bool

(>) :: Refined ps a -> Refined ps a -> Bool

(>=) :: Refined ps a -> Refined ps a -> Bool

max :: Refined ps a -> Refined ps a -> Refined ps a

min :: Refined ps a -> Refined ps a -> Refined ps a

Show a => Show (Refined ps a)

Methods

showsPrec :: Int -> Refined ps a -> ShowS

show :: Refined ps a -> String

showList :: [Refined ps a] -> ShowS

Lift a => Lift (Refined ps a)

Methods

lift :: Refined ps a -> Q Exp

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.

unrefined :: Refined ps a -> a

We can erase information we know by using unrefined.

Properties

class (Show a, Generic p) => Prop a p where

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

Minimal complete definition

checkProp

Associated Types

type PropProjection a p :: *

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

Methods

checkProp :: Proxy p -> a -> Either String (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.

Instances

Show a => Prop a IdProp

Every type has the identity property which allows to treat that type as well… that type.

Associated Types

type PropProjection a IdProp :: *

Methods

checkProp :: Proxy * IdProp -> a -> Either String (PropProjection a IdProp)

(Prop (PropProjection a p) t, Prop a p) => Prop a (Via t p)

Associated Types

type PropProjection a (Via t p) :: *

Methods

checkProp :: Proxy * (Via t p) -> a -> Either String (PropProjection a (Via t p))

data IdProp

Identity property. This is the identity in the category of refined types.

Instances

Generic IdProp

Associated Types

type Rep IdProp :: * -> *

Methods

from :: IdProp -> Rep IdProp x

to :: Rep IdProp x -> IdProp

Show a => Prop a IdProp

Every type has the identity property which allows to treat that type as well… that type.

Associated Types

type PropProjection a IdProp :: *

Methods

checkProp :: Proxy * IdProp -> a -> Either String (PropProjection a IdProp)

Axiom "id_prop" ([] *) ([] *) IdProp

We always can assume that a value has IdProp.

Axiom "id_prop_post'" ((:) * a ([] *)) ((:) * (Via IdProp a) ([] *)) a

Post-composition of IdProp can be dropped.

Axiom "id_prop_pre'" ((:) * a ([] *)) ((:) * (Via a IdProp) ([] *)) a

Pre-composition of IdProp can be dropped.

Axiom "id_prop_post" ((:) * a ([] *)) ((:) * a ([] *)) (Via IdProp a)

An existing prperty can be post-composed with IdProp.

Axiom "id_prop_pre" ((:) * a ([] *)) ((:) * a ([] *)) (Via a IdProp)

An existing property can be pre-composed with IdProp.

type Rep IdProp

type Rep IdProp = D1 * (MetaData "IdProp" "Data.Refined" "facts-0.0.1.0-AbEeMlT9VkaDHYIx98XSgl" False) (V1 *)

type PropProjection a IdProp

type PropProjection a IdProp = a

type family PropName (p :: *) :: Symbol where ...

Obtain a name of property type as a type of the kind Symbol.

Equations

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

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.

Equations

AddProp '[] p = '[p]

AddProp (n ': ps) p = AddPropC (CmpSymbol (PropName p) (PropName n)) p n ps

type family HasProp (ps :: [*]) (p :: *) :: Constraint where ...

The resulting constraint will be satisfied iff the collection of properties ps has the property p is it.

Equations

HasProp '[] p = TypeError (ShowType p :<>: Text " is not a proven property")

HasProp (p ': ps) p = ()

HasProp (b ': ps) p = HasProp ps p

type family HasProps (ps :: [*]) (qs :: [*]) :: Constraint where ...

Like HasProp but for many properties at once.

Equations

HasProps ps '[] = ()

HasProps ps (q ': qs) = (HasProp ps q, HasProps ps qs)

type family ProjectionProps (ps :: [*]) (p :: *) :: [*] where ...

Construct a list of properties from ps for projection obtained via p.

Equations

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

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)

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)

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)

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

Establish a property at compile time using Template Haskell.

data RefinedException

Exception that is thrown at run time when a property doesn't hold.

Constructors

RefinedException

Fields

• 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

Instances

Show RefinedException

Methods

showsPrec :: Int -> RefinedException -> ShowS

show :: RefinedException -> String

showList :: [RefinedException] -> ShowS

Exception RefinedException

Methods

toException :: RefinedException -> SomeException

fromException :: SomeException -> Maybe RefinedException

displayException :: RefinedException -> String

Following properties

data Via (t :: *) (p :: *) infixl 5

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 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 to state Axioms (see below) that talk about properties of “connected” types. Without Via, Axioms could only talk about relations between properties of the same type.

Instances

(Prop (PropProjection a p) t, Prop a p) => Prop a (Via t p)

Associated Types

type PropProjection a (Via t p) :: *

Methods

checkProp :: Proxy * (Via t p) -> a -> Either String (PropProjection a (Via t p))

Axiom "id_prop_post'" ((:) * a ([] *)) ((:) * (Via IdProp a) ([] *)) a

Post-composition of IdProp can be dropped.

Axiom "id_prop_pre'" ((:) * a ([] *)) ((:) * (Via a IdProp) ([] *)) a

Pre-composition of IdProp can be dropped.

Axiom "id_prop_post" ((:) * a ([] *)) ((:) * a ([] *)) (Via IdProp a)

An existing prperty can be post-composed with IdProp.

Axiom "id_prop_pre" ((:) * a ([] *)) ((:) * a ([] *)) (Via a IdProp)

An existing property can be pre-composed with IdProp.

Generic (Via t p)

Associated Types

type Rep (Via t p) :: * -> *

Methods

from :: Via t p -> Rep (Via t p) x

to :: Rep (Via t p) x -> Via t p

type PropProjection a (Via t p)

type PropProjection a (Via t p) = PropProjection (PropProjection a p) t

type Rep (Via t p)

type Rep (Via t p) = D1 * (MetaData "Via" "Data.Refined" "facts-0.0.1.0-AbEeMlT9VkaDHYIx98XSgl" False) (V1 *)

followProp :: forall p ps a. (Prop a p, ps `HasProp` p, HasCallStack) => Refined ps a -> Refined (ProjectionProps ps p) (PropProjection a p)

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

An Axiom name vs qs p allows 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.

Instances

Axiom "id_prop" ([] *) ([] *) IdProp

We always can assume that a value has IdProp.

Axiom "id_prop_post'" ((:) * a ([] *)) ((:) * (Via IdProp a) ([] *)) a

Post-composition of IdProp can be dropped.

Axiom "id_prop_pre'" ((:) * a ([] *)) ((:) * (Via a IdProp) ([] *)) a

Pre-composition of IdProp can be dropped.

Axiom "id_prop_post" ((:) * a ([] *)) ((:) * a ([] *)) (Via IdProp a)

An existing prperty can be post-composed with IdProp.

Axiom "id_prop_pre" ((:) * a ([] *)) ((:) * a ([] *)) (Via a IdProp)

An existing property can be pre-composed with IdProp.

data V (a :: k)

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

Apply Axiom and deduce a new property.

selectProps :: forall qs ps a. ps `HasProps` qs => Refined ps a -> Refined qs a

Select some properties from known properties.