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 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 (p a) b => Known k (Flip k k p b) a 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 | |
((~) ((,) 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 | |
type WitnessC ØC (Known N Nat n) (Nat n) = ØC | |
type WitnessC ØC (Known N Nat n) (VT k n f a) = ØC |