Copyright	Copyright (C) 2015 Kyle Carter
License	BSD3
Maintainer	Kyle Carter <kylcarte@indiana.edu>
Stability	experimental
Portability	RankNTypes
Safe Haskell	None
Language	Haskell2010

Type.Class.Witness

Description

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.

Synopsis

Documentation

data Wit :: Constraint -> * where Source #

A reified Constraint.

Constructors

Wit :: c => Wit c

Instances

c => Known Constraint Wit c Source #	If the constraint `c` holds, there is a canonical construction for a term of type `Wit c`, viz. the constructor `Wit`.
Associated Types type KnownC Wit (c :: Wit -> *) (a :: Wit) :: Constraint Source # Methods known :: c a Source #
Witness ØC c (Wit c) Source #
Associated Types type WitnessC (ØC :: Constraint) (c :: Constraint) (Wit c) :: Constraint Source # Methods (\\) :: ØC => (c -> r) -> Wit c -> r Source #
type KnownC Constraint Wit c Source #
type KnownC Constraint Wit c = c
type WitnessC ØC c (Wit c) Source #
type WitnessC ØC c (Wit c) = ØC

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

Constructors

Wit1 :: c a => Wit1 c a

Instances

Witness ØC (c a) (Wit1 k c a) Source #
Associated Types type WitnessC (ØC :: Constraint) (c a :: Constraint) (Wit1 k c a) :: Constraint Source # Methods (\\) :: ØC => (c a -> r) -> Wit1 k c a -> r Source #
c a => Known k (Wit1 k c) a Source #
Associated Types type KnownC (Wit1 k c) (a :: Wit1 k c -> *) (a :: Wit1 k c) :: Constraint Source # Methods known :: a a Source #
type WitnessC ØC (c a) (Wit1 k c a) Source #
type WitnessC ØC (c a) (Wit1 k c a) = ØC
type KnownC k (Wit1 k c) a Source #
type KnownC k (Wit1 k c) a = c a

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

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 :- q
Fields getSub :: p => Wit q

Instances

Category Constraint (:-) Source #
Methods id :: cat a a # (.) :: cat b c -> cat a b -> cat a c #
Witness p q ((:-) p q) Source #	An entailment `p :- q` is a Witness of `q`, given `p`.
Associated Types type WitnessC (p :: Constraint) (q :: Constraint) ((:-) p q) :: Constraint Source # Methods (\\) :: p => (q -> r) -> (p :- q) -> r Source #
type WitnessC p q ((:-) p q) Source #
type WitnessC p q ((:-) p q) = ØC

transC :: (b :- c) -> (a :- b) -> a :- c Source #

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

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.

Minimal complete definition

(\\)

Associated Types

type WitnessC p q t :: Constraint Source #

Methods

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

Instances

Witness p q a => Witness p q (I a) Source #
Associated Types type WitnessC (p :: Constraint) (q :: Constraint) (I a) :: Constraint Source # Methods (\\) :: p => (q -> r) -> I a -> r Source #
Witness ØC c (Wit c) Source #
Associated Types type WitnessC (ØC :: Constraint) (c :: Constraint) (Wit c) :: Constraint Source # Methods (\\) :: ØC => (c -> r) -> Wit c -> r Source #
Witness p q ((:-) p q) Source #	An entailment `p :- q` is a Witness of `q`, given `p`.
Associated Types type WitnessC (p :: Constraint) (q :: Constraint) ((:-) p q) :: Constraint Source # Methods (\\) :: p => (q -> r) -> (p :- q) -> r Source #
Witness p q (f a a) => Witness p q (Join k f a) Source #
Associated Types type WitnessC (p :: Constraint) (q :: Constraint) (Join k f a) :: Constraint Source # Methods (\\) :: p => (q -> r) -> Join k f a -> r Source #
Witness p q r => Witness p q (C k r a) Source #
Associated Types type WitnessC (p :: Constraint) (q :: Constraint) (C k r a) :: Constraint Source # Methods (\\) :: p => (q -> r) -> C k r a -> r Source #
(Witness p q (f a1), Witness p q (Sum a f ((:<) a b as))) => Witness p q (Sum a f ((:<) a a1 ((:<) a b as))) Source #
Associated Types type WitnessC (p :: Constraint) (q :: Constraint) (Sum a f ((:<) a a1 ((:<) a b as))) :: Constraint Source # Methods (\\) :: p => (q -> r) -> Sum a f ((a :< a1) ((a :< b) as)) -> r Source #
Witness p q (f a) => Witness p q (Sum k f ((:) k a ([] k))) Source #
Associated Types type WitnessC (p :: Constraint) (q :: Constraint) (Sum k f ((:) k a ([] k))) :: Constraint Source # Methods (\\) :: p => (q -> r) -> Sum k f ((k ': a) [k]) -> r Source #
(Witness p q (f a), (~) (Maybe k) x (Just k a)) => Witness p q (Option k f x) Source #
Associated Types type WitnessC (p :: Constraint) (q :: Constraint) (Option k f x) :: Constraint Source # Methods (\\) :: p => (q -> r) -> Option k f x -> r Source #
Witness ØC ØC (FProd k (Ø (k -> *)) a) Source #	An empty FProd is a no-op Witness.
Associated Types type WitnessC (ØC :: Constraint) (ØC :: Constraint) (FProd k (Ø (k -> )) a) :: Constraint Source # Methods (\\) :: ØC => (ØC -> r) -> FProd k (Ø (k -> )) a -> r Source #
Witness ØC ØC (Prod k f (Ø k)) Source #
Associated Types type WitnessC (ØC :: Constraint) (ØC :: Constraint) (Prod k f (Ø k)) :: Constraint Source # Methods (\\) :: ØC => (ØC -> r) -> Prod k f (Ø k) -> r Source #
(Witness r s (p a b), (~) (k, l) q ((#) k l a b)) => Witness r s (Uncur l k p q) Source #
Associated Types type WitnessC (r :: Constraint) (s :: Constraint) (Uncur l k p q) :: Constraint Source # Methods (\\) :: r => (s -> r) -> Uncur l k p q -> r Source #
(Witness p q (f a), Witness p q (g a)) => Witness p q ((:\|:) k f g a) Source #
Associated Types type WitnessC (p :: Constraint) (q :: Constraint) ((:\|:) k f g a) :: Constraint Source # Methods (\\) :: p => (q -> r) -> (k :\|: f) g a -> r Source #
(Witness r s (p a b c), (~) (k, l, m) q ((,,) k l m a b c)) => Witness r s (Uncur3 m l k p q) Source #
Associated Types type WitnessC (r :: Constraint) (s :: Constraint) (Uncur3 m l k p q) :: Constraint Source # Methods (\\) :: r => (s -> r) -> Uncur3 m l k p q -> r Source #
Witness q r (p ((#) k l a b)) => Witness q r (Cur k l p a b) Source #
Associated Types type WitnessC (q :: Constraint) (r :: Constraint) (Cur k l p a b) :: Constraint Source # Methods (\\) :: q => (r -> r) -> Cur k l p a b -> r Source #
Witness p q (f a b) => Witness p q (Flip k k1 f b a) Source #
Associated Types type WitnessC (p :: Constraint) (q :: Constraint) (Flip k k1 f b a) :: Constraint Source # Methods (\\) :: p => (q -> r) -> Flip k k1 f b a -> r Source #
Witness p q (f (g a)) => Witness p q ((:.:) k l f g a) Source #
Associated Types type WitnessC (p :: Constraint) (q :: Constraint) ((:.:) k l f g a) :: Constraint Source # Methods (\\) :: p => (q -> r) -> (k :.: l) f g a -> r Source #
Witness p q (g b1) => Witness p q ((:+:) b k f g (Right k b b1)) Source #
Associated Types type WitnessC (p :: Constraint) (q :: Constraint) ((:+:) b k f g (Right k b b1)) :: Constraint Source # Methods (\\) :: p => (q -> r) -> (b :+: k) f g (Right k b b1) -> r Source #
Witness p q (f a1) => Witness p q ((:+:) l a f g (Left a l a1)) Source #
Associated Types type WitnessC (p :: Constraint) (q :: Constraint) ((:+:) l a f g (Left a l a1)) :: Constraint Source # Methods (\\) :: p => (q -> r) -> (l :+: a) f g (Left a l a1) -> r Source #
Witness q r (p ((,,) k l m a b c)) => Witness q r (Cur3 k l m p a b c) Source #
Associated Types type WitnessC (q :: Constraint) (r :: Constraint) (Cur3 k l m p a b c) :: Constraint Source # Methods (\\) :: q => (r -> r) -> Cur3 k l m p a b c -> r Source #
Witness ØC (c a) (Wit1 k c a) Source #
Associated Types type WitnessC (ØC :: Constraint) (c a :: Constraint) (Wit1 k c a) :: Constraint Source # Methods (\\) :: ØC => (c a -> r) -> Wit1 k c a -> r Source #
(~) N n (Len k as) => Witness ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) Source #
Associated Types type WitnessC (ØC :: Constraint) ((Known N Nat n, Known [k] (Length k) as) :: Constraint) (Length k as) :: Constraint Source # Methods (\\) :: ØC => ((Known N Nat n, Known [k] (Length k) as) -> r) -> Length k as -> r Source #
(~) N n' (Pred n) => Witness ØC ((~) N (S n') n) (Fin n) Source #	A `Fin n` is a `Witness` that `n >= 1`. That is, `Pred n` is well defined.
Associated Types type WitnessC (ØC :: Constraint) ((~) N (S n') n :: Constraint) (Fin n) :: Constraint Source # Methods (\\) :: ØC => ((N ~ S n') n -> r) -> Fin n -> r Source #
Witness ØC (Known N Nat n) (Nat n) Source #	A `Nat n` is a `Witness` that there is a canonical construction for `Nat n`.
Associated Types type WitnessC (ØC :: Constraint) (Known N Nat n :: Constraint) (Nat n) :: Constraint Source # Methods (\\) :: ØC => (Known N Nat n -> r) -> Nat n -> r Source #
(~) N x' (Pred x) => Witness ØC ((~) N (S x') x) (IFin x y) Source #	An `IFin x y` is a `Witness` that `x >= 1`. That is, `Pred x` is well defined.
Associated Types type WitnessC (ØC :: Constraint) ((~) N (S x') x :: Constraint) (IFin x y) :: Constraint Source # Methods (\\) :: ØC => ((N ~ S x') x -> r) -> IFin x y -> r Source #
Witness ØC ((~) k a b) ((:~:) k a b) Source #	A type equality `a :~: b` is a Witness that `(a ~ b)`.
Associated Types type WitnessC (ØC :: Constraint) ((~) k a b :: Constraint) ((:~:) k a b) :: Constraint Source # Methods (\\) :: ØC => ((k ~ a) b -> r) -> (k :~: a) b -> r Source #
Witness ØC (Elem k as a) (Index k as a) Source #
Associated Types type WitnessC (ØC :: Constraint) (Elem k as a :: Constraint) (Index k as a) :: Constraint Source # Methods (\\) :: ØC => (Elem k as a -> r) -> Index k as a -> r Source #
Witness ØC (Known N Nat n) (VecT k n f a) Source #
Associated Types type WitnessC (ØC :: Constraint) (Known N Nat n :: Constraint) (VecT k n f a) :: Constraint Source # Methods (\\) :: ØC => (Known N Nat n -> r) -> VecT k n f a -> r Source #
Witness ØC (Without k as a bs) (Remove k as a bs) Source #
Associated Types type WitnessC (ØC :: Constraint) (Without k as a bs :: Constraint) (Remove k as a bs) :: Constraint Source # Methods (\\) :: ØC => (Without k as a bs -> r) -> Remove k as a bs -> r Source #
Witness ØC (WithoutAll k as bs cs) (Difference k as bs cs) Source #
Associated Types type WitnessC (ØC :: Constraint) (WithoutAll k as bs cs :: Constraint) (Difference k as bs cs) :: Constraint Source # Methods (\\) :: ØC => (WithoutAll k as bs cs -> r) -> Difference k as bs cs -> r Source #
((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N x' (Pred x)) => Witness ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y) Source #
Associated Types type WitnessC (ØC :: Constraint) (((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) :: Constraint) (NatGT x y) :: Constraint Source # Methods (\\) :: ØC => (((N ~ x) (S x'), Known N Nat y, (Bool ~ lt) False, (Bool ~ eq) False, (Bool ~ gt) True) -> r) -> NatGT x y -> r Source #
((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y)) => Witness ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y) Source #
Associated Types type WitnessC (ØC :: Constraint) (((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) :: Constraint) (NatEQ x y) :: Constraint Source # Methods (\\) :: ØC => (((N ~ x) y, Known N Nat x, (Bool ~ lt) False, (Bool ~ eq) True, (Bool ~ gt) False) -> r) -> NatEQ x y -> r Source #
((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N y' (Pred y)) => Witness ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y) Source #
Associated Types type WitnessC (ØC :: Constraint) (((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) :: Constraint) (NatLT x y) :: Constraint Source # Methods (\\) :: ØC => (((N ~ y) (S y'), Known N Nat x, (Bool ~ lt) True, (Bool ~ eq) False, (Bool ~ gt) False) -> r) -> NatLT x y -> r Source #
(Witness p q (f a), Witness s t (FProd k fs a)) => Witness (p, s) (q, t) (FProd k ((:<) (k -> *) f fs) a) Source #	A non-empty FProd is a Witness if both its head and tail are Witnesses.
Associated Types type WitnessC ((p, s) :: Constraint) ((q, t) :: Constraint) (FProd k ((:<) (k -> ) f fs) a) :: Constraint Source # Methods (\\) :: (p, s) => ((q, t) -> r) -> FProd k (((k -> ) :< f) fs) a -> r Source #
(Witness p q (f a1), Witness s t (Prod a f as)) => Witness (p, s) (q, t) (Prod a f ((:<) a a1 as)) Source #
Associated Types type WitnessC ((p, s) :: Constraint) ((q, t) :: Constraint) (Prod a f ((:<) a a1 as)) :: Constraint Source # Methods (\\) :: (p, s) => ((q, t) -> r) -> Prod a f ((a :< a1) as) -> r Source #
(Witness p q (f a), Witness s t (g a)) => Witness (p, s) (q, t) ((:&:) k f g a) Source #
Associated Types type WitnessC ((p, s) :: Constraint) ((q, t) :: Constraint) ((:&:) k f g a) :: Constraint Source # Methods (\\) :: (p, s) => ((q, t) -> r) -> (k :&: f) g a -> r Source #
(Witness p q (f a), Witness s t (g b), (~) (k, l) x ((#) k l a b)) => Witness (p, s) (q, t) ((:*:) l k f g x) Source #
Associated Types type WitnessC ((p, s) :: Constraint) ((q, t) :: Constraint) ((::) l k f g x) :: Constraint Source # Methods (\\) :: (p, s) => ((q, t) -> r) -> (l :: k) f g x -> r Source #

(//) :: (Witness p q t, p) => t -> (q => r) -> r infixr 0 Source #

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

Convert a Witness to a canonical reified Constraint.

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

Convert a Witness to a canonical reified entailment.

class Fails c where Source #

Minimal complete definition

failC

Methods

failC :: c :- Fail Source #

absurdC :: Fails a => a :- b Source #

class c => Const c d where Source #

Minimal complete definition

constC

Methods

constC :: Wit c Source #

Instances

c => Const k c d Source #
Methods constC :: Wit d Source #

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

Minimal complete definition

compC

Methods

compC :: Wit (f (g a)) Source #

Instances

f (g a) => (∘) k l f g a Source #
Methods compC :: Wit (a (g a)) Source #

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

Minimal complete definition

conjC

Methods

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

Instances

(f a, g a) => (∧) k f g a Source #
Methods conjC :: (Wit (g a), Wit (a a)) Source #

class (f ∨ g) a where infixr 6 Source #

Minimal complete definition

disjC

Methods

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

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

pureC :: b => a :- b Source #

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

class Forall p q where Source #

Methods

forall :: p a :- q a Source #

forall :: q a => p a :- q a Source #

toEquality :: ((a ~ b) :- (c ~ d)) -> (a :~: b) -> c :~: d Source #

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

type family Holds (b :: Bool) (c :: Constraint) :: Constraint where ... Source #

Equations

Holds True c = c
Holds False c = ØC

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

top :: a :- ØC Source #

bottom :: Fail :- c Source #

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

Constraint chaining under Maybe.

(//?+) :: (Witness p q t, p) => Either e t -> (q => Either e r) -> Either e r infixr 0 Source #

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

qed :: Maybe (a :~: a) Source #

impossible :: a -> Void Source #

exFalso :: Wit Fail -> a Source #

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

class TestEquality1 f where Source #

Minimal complete definition

testEquality1

Methods

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

Instances

TestEquality l1 f => TestEquality1 l (l -> l1) ((:.:) l l1 f) Source #
Methods testEquality1 :: f a c -> f b c -> Maybe ((k :~: a) b) Source #

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

data Dec a Source #

Constructors

Proven a
Refuted (a -> Void)

class DecEquality f where Source #

Minimal complete definition

decideEquality

Methods

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

Instances

(DecEquality k f, DecEquality l g) => DecEquality (k, l) ((:*:) l k f g) Source #
Methods decideEquality :: f a -> f b -> Dec (((l :*: k) f g :~: a) b) Source #

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

absurd :: Arrow p => p Void a Source #