Copyright | Copyright (C) 2015 Kyle Carter |
---|---|
License | BSD3 |
Maintainer | Kyle Carter <kylcarte@indiana.edu> |
Stability | experimental |
Portability | RankNTypes |
Safe Haskell | None |
Language | Haskell2010 |
A type t
that is a
provides a Witness
p q tConstraint
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.
- data Wit :: Constraint -> * where
- data Wit1 :: (k -> Constraint) -> k -> * where
- data (:-) :: Constraint -> Constraint -> * where
- transC :: (b :- c) -> (a :- b) -> a :- c
- class WitnessC p q t => Witness p q t | t -> p q where
- type WitnessC p q t :: Constraint
- (//) :: (Witness p q t, p) => t -> (q => r) -> r
- witnessed :: Witness ØC q t => t -> Wit q
- entailed :: Witness p q t => t -> p :- q
- class Fails c where
- absurdC :: Fails a => a :- b
- class c => Const c d where
- class f (g a) => (f ∘ g) a where
- class (f a, g a) => (f ∧ g) a where
- class (f ∨ g) a where
- 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
- toEquality :: ((a ~ b) :- (c ~ d)) -> (a :~: b) -> c :~: d
- commute :: (a ~ b) :- (b ~ a)
- type family Holds (b :: Bool) (c :: Constraint) :: Constraint where ...
- falso :: (b ~ False) :- Holds b c
- top :: a :- ØC
- bottom :: Fail :- c
- (//?) :: (Witness p q t, p) => Maybe t -> (q => Maybe r) -> Maybe r
- (//?+) :: (Witness p q t, p) => Either e t -> (q => Either e r) -> Either e r
- witMaybe :: (Witness p q t, p) => Maybe t -> (q => Maybe r) -> Maybe r -> Maybe r
- qed :: Maybe (a :~: a)
- impossible :: a -> Void
- exFalso :: Wit Fail -> a
- (=?=) :: TestEquality f => f a -> f b -> Maybe (a :~: b)
- class TestEquality1 f where
- (=??=) :: TestEquality1 f => f a c -> f b c -> Maybe (a :~: b)
- data Dec a
- class DecEquality f where
- decCase :: Dec a -> (a -> r) -> ((a -> Void) -> r) -> r
- absurd :: Arrow p => p Void a
Documentation
data Wit :: Constraint -> * where Source #
A reified Constraint
.
data Wit1 :: (k -> Constraint) -> k -> * where Source #
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 Constraint
s form a Category
:
>>>
id :: p :- p
>>>
(.) :: (q :- r) -> (p :-> q) -> (p :- r)
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
.
type WitnessC p q t :: Constraint Source #
Witness p q a => Witness p q (I a) Source # | |
Witness ØC c (Wit c) Source # | |
Witness p q ((:-) p q) Source # | An entailment |
Witness p q (f a a) => Witness p q (Join k f a) Source # | |
Witness p q r => Witness p q (C k r a) 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 # | |
Witness p q (f a) => Witness p q (Sum k f ((:) k a ([] k))) Source # | |
(Witness p q (f a), (~) (Maybe k) x (Just k a)) => Witness p q (Option k f x) Source # | |
Witness ØC ØC (FProd k (Ø (k -> *)) a) Source # | An empty FProd is a no-op Witness. |
Witness ØC ØC (Prod k f (Ø k)) Source # | |
(Witness r s (p a b), (~) (k, l) q ((#) k l a b)) => Witness r s (Uncur l k p q) Source # | |
(Witness p q (f a), Witness p q (g a)) => Witness p q ((:|:) k f g a) 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 # | |
Witness q r (p ((#) k l a b)) => Witness q r (Cur k l p a b) Source # | |
Witness p q (f a b) => Witness p q (Flip k k1 f b a) Source # | |
Witness p q (f (g a)) => Witness p q ((:.:) k l f g a) Source # | |
Witness p q (g b1) => Witness p q ((:+:) b k f g (Right k b b1)) Source # | |
Witness p q (f a1) => Witness p q ((:+:) l a f g (Left a l a1)) Source # | |
Witness q r (p ((,,) k l m a b c)) => Witness q r (Cur3 k l m p a b c) Source # | |
Witness ØC (c a) (Wit1 k c a) Source # | |
(~) N n (Len k as) => Witness ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) Source # | |
(~) N n' (Pred n) => Witness ØC ((~) N (S n') n) (Fin n) Source # | A That is, |
Witness ØC (Known N Nat n) (Nat n) Source # | A |
(~) N x' (Pred x) => Witness ØC ((~) N (S x') x) (IFin x y) Source # | An That is, |
Witness ØC ((~) k a b) ((:~:) k a b) Source # | A type equality |
Witness ØC (Elem k as a) (Index k as a) Source # | |
Witness ØC (Known N Nat n) (VecT k n f a) Source # | |
Witness ØC (Without k as a bs) (Remove k as a bs) Source # | |
Witness ØC (WithoutAll k as bs cs) (Difference k as bs cs) 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 # | |
((~) 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 # | |
((~) 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 # | |
(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. |
(Witness p q (f a1), Witness s t (Prod a f as)) => Witness (p, s) (q, t) (Prod a f ((:<) a a1 as)) Source # | |
(Witness p q (f a), Witness s t (g a)) => Witness (p, s) (q, t) ((:&:) k f g a) 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 # | |
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.
type family Holds (b :: Bool) (c :: Constraint) :: Constraint where ... Source #
(//?) :: (Witness p q t, p) => Maybe t -> (q => Maybe r) -> Maybe r infixr 0 Source #
Constraint chaining under Maybe
.
impossible :: a -> Void Source #
class TestEquality1 f where Source #
testEquality1 :: f a c -> f b c -> Maybe (a :~: b) Source #
TestEquality l1 f => TestEquality1 l (l -> l1) ((:.:) l l1 f) Source # | |
class DecEquality f where Source #
decideEquality :: f a -> f b -> Dec (a :~: b) Source #
(DecEquality k f, DecEquality l g) => DecEquality (k, l) ((:*:) l k f g) Source # | |