Copyright | Copyright (C) 2015 Kyle Carter |
---|---|
License | BSD3 |
Maintainer | Kyle Carter <kylcarte@indiana.edu> |
Stability | experimental |
Portability | RankNTypes |
Safe Haskell | None |
Language | Haskell2010 |
The Known
class, among others in this library, use an associated
Constraint
to maintain a bidirectional chain of inference.
For instance, given evidence of Known Nat n
, if n
later gets refined
to n'
, we can correctly infer Known Nat n'
, as per the type instance
defined for KnownC Nat (S n')
.
- class KnownC f a => Known f a where
- type KnownC f a :: Constraint
Documentation
class KnownC f a => Known f a where Source #
Each instance of Known
provides a canonical construction
of a type at a particular index.
Useful for working with singleton-esque GADTs.
type KnownC f a :: Constraint Source #
Known Bool Boolean False Source # | |
Known Bool Boolean True Source # | |
c => Known Constraint Wit c Source # | If the constraint |
Known N Nat Z Source # | |
Known N Nat n => Known N Nat (S n) Source # | If |
(~) k a b => Known k ((:~:) k a) b Source # | |
c a => Known k (Wit1 k c) a Source # | |
Known k (f a) a => Known k (Join k f) a Source # | |
(∈) k a as => Known k (Index k as) a Source # | |
(Known k f a, Known k (FProd k fs) a) => Known k (FProd k ((:<) (k -> *) f fs)) a Source # | |
Known k (FProd k (Ø (k -> *))) a Source # | |
(~) N n (Len k as) => Witness ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) Source # | |
(Known k f a, Known k g a) => Known k ((:&:) k f g) a Source # | |
Witness ØC (Known N Nat n) (Nat n) Source # | A |
Witness ØC (Known N Nat n) (VecT k n f a) Source # | |
Known (k1, k) p ((#) k1 k a b) => Known k (Cur k1 k p a) b Source # | |
Known k1 (p a) b => Known k (Flip k k1 p b) a 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 # | |
Known (k1, l, k) p ((,,) k1 l k a b c) => Known k (Cur3 k1 l k p a b) c Source # | |
Known [k] (Length k) (Ø k) Source # | |
Known [k] (Length k) as => Known [k] (Length k) ((:<) k a as) Source # | |
(Known [k] (Length k) as, Every k (Known k f) as) => Known [k] (Prod k f) as Source # | |
Known (Maybe k) (Option k f) (Nothing k) Source # | |
Known a f a1 => Known (Maybe a) (Option a f) (Just a a1) Source # | |
Without k as a bs => Known [k] (Remove k as a) bs Source # | |
WithoutAll k as bs cs => Known [k] (Difference k as bs) cs Source # | |
(Known l (p a) b, (~) (k, l) q ((#) k l a b)) => Known (k, l) (Uncur l k p) q Source # | |
((~) (k, l) p ((#) k l a b), Known k f a, Known l g b) => Known (k, l) ((:*:) l k f g) p Source # | |
Known b g b1 => Known (Either k b) ((:+:) b k f g) (Right k b b1) Source # | |
Known a f a1 => Known (Either a l) ((:+:) l a f g) (Left a l a1) Source # | |
(Known m (p a b) c, (~) (k, l, m) q ((,,) k l m a b c)) => Known (k, l, m) (Uncur3 m l k p) q Source # | |
type WitnessC ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) Source # | |
type WitnessC ØC (Known N Nat n) (Nat n) Source # | |
type WitnessC ØC (Known N Nat n) (VecT k n f a) Source # | |
type WitnessC ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y) Source # | |
type WitnessC ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y) Source # | |
type WitnessC ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y) Source # | |