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
- known :: f a
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
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 | |
Known k (Index k as) a => Known k (Index k ((:<) k b as)) a Source | |
Known k (Index k ((:<) k a as)) a Source | |
Known k (f a) a => Known k (Join k f) 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 | |
(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) (VT k n f a) Source | |
Known ((,) k1 k) p ((#) k1 k a b) => Known k (Cur k k p a) b Source | |
Known k1 (p a) b => Known k (Flip k k p b) a Source | |
Known ((,,) k1 k2 k) p ((,,) k1 k2 k a b c) => Known k (Cur3 k k 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] (Prod k f) (Ø k) Source | |
Known (Maybe k) (Option k f) (Nothing k) Source | |
Known k f a => Known (Maybe k) (Option k f) (Just k a) Source | |
(Known k f a, Known [k] (Prod k f) as) => Known [k] (Prod k f) ((:<) k a as) Source | |
(Known k1 (p a) b, (~) ((,) k k1) q ((#) k k1 a b)) => Known ((,) k k) (Uncur k k p) q Source | |
((~) ((,) k k1) p ((#) k k1 a b), Known k f a, Known k1 g b) => Known ((,) k k) ((:*:) k k f g) p Source | |
Known k1 g b => Known (Either k k) ((:|:) k k f g) (Right k k b) Source | |
Known k1 f a => Known (Either k k) ((:|:) k k f g) (Left k k a) Source | |
(Known k2 (p a b) c, (~) ((,,) k k1 k2) q ((,,) k k1 k2 a b c)) => Known ((,,) k k k) (Uncur3 k k k p) q Source | |
type WitnessC ØC (Known N Nat n) (Nat n) = ØC | |
type WitnessC ØC (Known N Nat n) (VT k n f a) = ØC |