Type.Class.Witness

A type t that is a Witness p q t provides a Constraint entailment of q, given that p holds.

The Witness class uses an associated Constraint WitnessC to maintain backwards inference of Witness instances with respect to type refinement. See the Known class for more information.

Heavily inspired by ekmett's constraints library: http://hackage.haskell.org/package/constraints

The code provided here does not quite subsume the constraints library, as we do not give classes and instances for representing the standard library's class heirarchy and instance definitions.

Documentation

data Wit :: Constraint -> * where

A reified Constraint.

Constructors

Wit :: c => Wit c

Instances

c => Known Constraint Wit c

If the constraint c holds, there is a canonical construction for a term of type Wit c, viz. the constructor Wit.

Witness ØC c (Wit c)

type KnownC Constraint Wit c = c

type WitnessC ØC c (Wit c) = ØC

data Wit1 :: (k -> Constraint) -> k -> * where

Constructors

Wit1 :: c a => Wit1 c a

data (:-) :: Constraint -> Constraint -> * where infixr 4

Reified evidence of Constraint entailment.

Given a term of p :- q, the Constraint q holds if p holds.

Entailment of Constraints form a Category:

>>> id  :: p :- p
>>> (.) :: (q :- r) -> (p :-> q) -> (p :- r)

Constructors

Sub :: (p => Wit q) -> p :- q

Fields

getSub :: p => Wit q

Instances

Category Constraint (:-)

Witness p q ((:-) p q)

An entailment p :- q is a Witness of q, given p.

type WitnessC p q ((:-) p q) = ØC

type (:-:) = Bij (:-) infixr 4

class WitnessC p q t => Witness p q t | t -> p q where

A general eliminator for entailment.

Given a term of type t with an instance Witness p q t and a term of type r that depends on Constraint q, we can reduce the Constraint to p.

If p is ØC, i.e. the empty Constraint (), then a Witness t can completely discharge the Constraint q.

Associated Types

type WitnessC p q t :: Constraint

Methods

(\\) :: p => (q => r) -> t -> r infixl 1

Instances

Witness p q a => Witness p q (I a)

Witness ØC c (Wit c)

Witness p q ((:-) p q)

An entailment p :- q is a Witness of q, given p.

(Witness p q (f a), (~) (Maybe k) x (Just k a)) => Witness p q (Option k f x)

(Witness p q (f a), Witness p q (Sum k f ((:<) k b as))) => Witness p q (Sum k f ((:<) k a ((:<) k b as)))

Witness p q (f a) => Witness p q (Sum k f ((:) k a ([] k)))

Witness p q (f a a) => Witness p q (Join k f a)

Witness p q r => Witness p q (C k r a)

Witness p q (f a) => Witness p q (IT k f a)

Witness ØC ØC (Prod k f (Ø k))

Witness ØC ØC (FProd k (Ø (k -> *)) a)

An empty FProd is a no-op Witness.

(Witness p q (f a), Witness p q (g a)) => Witness p q ((:+:) k f g a)

(Witness r s (p a b), (~) ((,) k k1) q ((#) k k1 a b)) => Witness r s (Uncur k k p q)

Witness p q (g b) => Witness p q ((:|:) k k f g (Right k k b))

Witness p q (f a) => Witness p q ((:|:) k k f g (Left k k a))

(Witness r s (p a b c), (~) ((,,) k k1 k2) q ((,,) k k1 k2 a b c)) => Witness r s (Uncur3 k k k p q)

Witness q r (p ((#) k k1 a b)) => Witness q r (Cur k k p a b)

Witness p q (f a b) => Witness p q (Flip k k f b a)

Witness p q r => Witness p q (CT k k r f a)

Witness p q (f a (g a)) => Witness p q (SS k k f g a)

Witness p q (f (g a)) => Witness p q (RR k k g f a)

Witness p q (f (g a)) => Witness p q (LL k k a f g)

Witness p q (f (g a)) => Witness p q ((:.:) k k f g a)

Witness q r (p ((,,) k k1 k2 a b c)) => Witness q r (Cur3 k k k p a b c)

Witness p q (f (g a b)) => Witness p q ((:..:) k k k f g a b)

(~) N n' (Pred n) => Witness ØC ((~) N (S n') n) (Fin n)

A Fin n is a Witness that n >= 1.

That is, Pred n is well defined.

Witness ØC (Known N Nat n) (Nat n)

A Nat n is a Witness that there is a canonical construction for Nat n.

Witness ØC ((~) k a b) ((:~:) k a b)

A type equality a :~: b is a Witness that (a ~ b).

Witness ØC (Known N Nat n) (VT k n f a)

(Witness p q (f a), Witness s t (Prod k f as)) => Witness (p, s) (q, t) (Prod k f ((:<) k a as))

(Witness p q (f a), Witness s t (FProd k fs a)) => Witness (p, s) (q, t) (FProd k ((:<) (k -> *) f fs) a)

A non-empty FProd is a Witness if both its head and tail are Witnesses.

(Witness p q (f a), Witness s t (g a)) => Witness (p, s) (q, t) ((:&:) k f g a)

(Witness p q (f a), Witness s t (g b), (~) ((,) k k1) x ((#) k k1 a b)) => Witness (p, s) (q, t) ((:*:) k k f g x)

entailed :: Witness p q t => t -> p :- q

Convert a Witness to a canonical reified entailment.

witnessed :: Witness ØC q t => t -> Wit q

Convert a Witness to a canonical reified Constraint.

(/?) :: (Witness p q t, p) => Maybe t -> (q => Maybe r) -> Maybe r infixr 0

Constraint chaining under Maybe.

qed :: Maybe (a :~: a)

impossible :: a -> Void

data Dec a

Constructors

Proven a

Refuted (a -> Void)

class DecEquality f where

Methods

decideEquality :: f a -> f b -> Dec (a :~: b)

Instances

DecEquality N Nat

DecEquality k f => DecEquality k ((:&:) k f g)

(DecEquality k f, DecEquality k1 g) => DecEquality ((,) k k) ((:*:) k k f g)

decCase :: Dec a -> (a -> r) -> ((a -> Void) -> r) -> r

data Bij p a b

Constructors

Bij

Fields

fwd :: p a b

bwd :: p b a

Instances

Category k p => Category k (Bij k p)

($->) :: Bij p a b -> p a b infixr 1

(<-$) :: Bij p a b -> p b a infixr 1

type (<->) = Bij (->) infixr 5

(<->) :: p a b -> p b a -> Bij p a b infixr 5

(<?>) :: (r <-> s) -> Dec r -> Dec s infix 3