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.

refined creates a refined type with no associated properties. We don't demand anything, and so quite conveniently this is a pure function.

We can erase information we know by using unrefined.

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

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

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

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.

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

Like HasProp but for many properties at once.

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

Assume a property. This is unsafe and may be a source of bugs. Only use when you 100% sure that the property indeed holds.

Establish a property in a MonadThrow instance.

Establish a property in a MonadFail instance.

Establish a property in a MonadError instance.

Establish a property at compile time using Template Haskell.

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

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.

Obtain a projection as a refined value, i.e. follow a morphism created by a property.

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.

A helper wrapper to help us construct heterogeneous type-level lists with respect to kinds of elements.

Apply Axiom and deduce a new property.

Select some properties from known properties.