Copyright	(c) Matt Noonan 2018
License	BSD-style
Maintainer	matt.noonan@gmail.com
Portability	portable
Safe Haskell	None
Language	Haskell2010

Data.Refined

Contents

Refinement types
- Attaching arbitrary propositions to values
- Refinement types
  - Forgetting and re-introducing names
  - Traversals over collections of refined types

Description

Synopsis

data a ::: p
(...) :: a -> Proof p -> a ::: p
(...>) :: (a ::: p) -> (p -> Proof q) -> a ::: q
($:) :: (a -> b) -> (a ::: p) -> b ::: p
exorcise :: (a ::: p) -> a
conjure :: (a ::: p) -> Proof p
data Satisfies (p :: * -> *) a
type (?) a p = Satisfies p a
assert :: Defining (p ()) => a -> a ? p
unname :: ((a ~~ name) ::: p name) -> a ? p
rename :: (a ? p) -> (forall name. ((a ~~ name) ::: p name) -> t) -> t
(...?) :: (forall name. (a ~~ name) -> b ~~ f name) -> (forall name. p name -> Proof (q (f name))) -> (a ? p) -> b ? q
traverseP :: (Traversable t, Applicative f) => (forall name. ((a ~~ name) ::: p name) -> f b) -> t (a ? p) -> f (t b)
traverseP_ :: (Foldable t, Applicative f) => (forall name. ((a ~~ name) ::: p name) -> f b) -> t (a ? p) -> f ()
forP :: (Traversable t, Applicative f) => t (a ? p) -> (forall name. ((a ~~ name) ::: p name) -> f b) -> f (t b)
forP_ :: (Foldable t, Applicative f) => t (a ? p) -> (forall name. ((a ~~ name) ::: p name) -> f b) -> f ()

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 #
Instance details Defined in Data.Refined 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 #
Instance details Defined in Data.Refined 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.