Data.Refined

Refinement types

Attaching arbitrary propositions to values

data a ::: p infixr 1

Given a type a and a proposition p, the type (a ::: p) represents a value of type a, with an attached "ghost proof" of p.

Values of the type (a ::: p) have the same run-time representation as values of the normal type a; the proposition p does not carry a run-time space or time cost.

Instances

The a' a => The ((:::) a' p) a

Methods

the :: (a' ::: p) -> a

(...) :: a -> Proof p -> a ::: p

Given a value and a proof, attach the proof as a ghost proof on the value.

(...>) :: (a ::: p) -> (p -> Proof q) -> a ::: q

Apply an implication to the ghost proof attached to a value, leaving the value unchanged.

($:) :: (a -> b) -> (a ::: p) -> b ::: p

Given a value and a proof, apply a function to the value but leave the proof unchanged.

exorcise :: (a ::: p) -> a

Forget the ghost proof attached to a value.

conjure :: (a ::: p) -> Proof p

Extract the ghost proof from a value.

Refinement types

data Satisfies (p :: * -> *) a

Given a type a and a predicate p, the type a ?p represents a refinement type for a. Values of type a ?p should be values of type a that satisfy the predicate p.

Values of type a ?p have the same run-time representation as values of type a; the proposition p does not carry a run-time space or time cost.

Instances

The (Satisfies p a) a

Methods

the :: Satisfies p a -> a

type (?) a p = Satisfies p a infixr 1

An infix alias for Satisfies.

assert :: Defining (p ()) => a -> a ? p

For library authors: assert that a property holds.

Forgetting and re-introducing names

unname :: ((a ~~ name) ::: p name) -> a ? p

Existential introduction for names: given a named value of type a that satisfies a predicate p, coerce to a value of type a ?p.

rename :: (a ? p) -> (forall name. ((a ~~ name) ::: p name) -> t) -> t

Existential elimination for names: given a value of type a ?p, re-introduce a new name to produce a value of type a ~~ name ::: p name.

(...?) :: (forall name. (a ~~ name) -> b ~~ f name) -> (forall name. p name -> Proof (q (f name))) -> (a ? p) -> b ? q

Take a simple function with one named argument and a named return, plus an implication relating a precondition to a postcondition of the function, and produce a function between refined input and output types.

newtype NonEmpty xs = NonEmpty Defn
newtype Reverse  xs = Reverse  Defn

rev :: ([a] ~~ xs) -> ([a] ~~ Reverse xs)
rev xs = defn (reverse (the xs))

rev_nonempty_lemma :: NonEmpty xs -> Proof (NonEmpty (Reverse xs))

rev' :: ([a] ?NonEmpty) -> ([a] ?NonEmpty)
rev' = rev ...? rev_nonempty_lemma

Traversals over collections of refined types

traverseP :: (Traversable t, Applicative f) => (forall name. ((a ~~ name) ::: p name) -> f b) -> t (a ? p) -> f (t b)

Traverse a collection of refined values, re-introducing names in the body of the action.

traverseP_ :: (Foldable t, Applicative f) => (forall name. ((a ~~ name) ::: p name) -> f b) -> t (a ? p) -> f ()

Same as traverseP, but ignores the action's return value.

forP :: (Traversable t, Applicative f) => t (a ? p) -> (forall name. ((a ~~ name) ::: p name) -> f b) -> f (t b)

Same as traverse, with the argument order flipped.

forP_ :: (Foldable t, Applicative f) => t (a ? p) -> (forall name. ((a ~~ name) ::: p name) -> f b) -> f ()

Same as traverse_, with the argument order flipped.