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 t`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.

- 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 # | |