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

Instances

Witness ØC (c a) (Wit1 k c a)

c a => Known k (Wit1 k c) a

type WitnessC ØC (c a) (Wit1 k c a) = ØC

type KnownC k (Wit1 k c) a = 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

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 ØC ØC (FProd k (Ø (k -> *)) a)

An empty FProd is a no-op Witness.

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

(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 (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 ØC (KnownSymbol x) (Sym x)

Witness ØC (c a) (Wit1 k c a)

(~) 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 (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 (Prod k f as)) => Witness (p, s) (q, t) (Prod k f ((:<) k a as))

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

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

Convert a Witness to a canonical reified Constraint.

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

Convert a Witness to a canonical reified entailment.

class Fails c where

Methods

failC :: c :- Fail

absurdC :: Fails a => a :- b

class c => Const c d where

Methods

constC :: Wit c

Instances

c => Const k c d

class f (g a) => (f ∘ g) a where infixr 9

Methods

compC :: Wit (f (g a))

Instances

f (g a) => (∘) k k f g a

class (f a, g a) => (f ∧ g) a where infixr 7

Methods

conjC :: (Wit (f a), Wit (g a))

Instances

(f a, g a) => (∧) k f g a

class (f ∨ g) a where infixr 6

Methods

disjC :: Either (Wit (f a)) (Wit (g a))

eitherC :: forall f g a b. (f a :- b) -> (g a :- b) -> (f ∨ g) a :- b

pureC :: b => a :- b

contraC :: (a :- Fail) -> a :- b

class Forall p q where

Minimal complete definition

Nothing

Methods

forall :: p a :- q a

commute :: (a ~ b) :- (b ~ a)

type family Holds b c :: Constraint

Equations

Holds True c = c

Holds False c = ØC

falso :: (b ~ False) :- Holds b c

top :: a :- ØC

type Fail = True ~ False

bottom :: Fail :- c

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

Constraint chaining under Maybe.

witMaybe :: (Witness p q t, p) => Maybe t -> (q => Maybe r) -> Maybe r -> Maybe r

qed :: Maybe (a :~: a)

impossible :: a -> Void

(=?=) :: TestEquality f => f a -> f b -> Maybe (a :~: b) infix 4

class TestEquality1 f where

Methods

testEquality1 :: f a c -> f b c -> Maybe (a :~: b)

Instances

TestEquality k1 f => TestEquality1 (k -> k) k ((:.:) k k f)

(=??=) :: TestEquality1 f => f a c -> f b c -> Maybe (a :~: b) infix 4

data Dec a

Constructors

Proven a

Refuted (a -> Void)

class DecEquality f where

Methods

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

Instances

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

absurd :: Arrow p => p Void a