Type.Class.Known

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').

Documentation

class KnownC f a => Known f a where

Each instance of Known provides a canonical construction of a type at a particular index.

Useful for working with singleton-esque GADTs.

Associated Types

type KnownC f a :: Constraint

Methods

known :: f a

Instances

c => Known Constraint Wit c

If the constraint c holds, there is a canonical construction for a term of type Wit c, viz. the constructor Wit.

Known N Nat Z

Z_ is the canonical construction of a Nat Z.

Known N Nat n => Known N Nat (S n)

If n is a canonical construction of Nat n, S_ n is the canonical construction of Nat (S n).

(~) k a b => Known k ((:~:) k a) b

Known k (Index k as) a => Known k (Index k ((:<) k b as)) a

Known k (Index k ((:<) k a as)) a

Known k (f a) a => Known k (Join k f) a

(Known k f a, Known k (FProd k fs) a) => Known k (FProd k ((:<) (k -> *) f fs)) a

Known k (FProd k (Ø (k -> *))) a

(Known k f a, Known k g a) => Known k ((:&:) k f g) a

Witness ØC (Known N Nat n) (Nat n)

A Nat n is a Witness that there is a canonical construction for Nat n.

Witness ØC (Known N Nat n) (VT k n f a)

Known ((,) k1 k) p ((#) k1 k a b) => Known k (Cur k k p a) b

Known k1 (p a) b => Known k (Flip k k p b) a

Known ((,,) k1 k2 k) p ((,,) k1 k2 k a b c) => Known k (Cur3 k k k p a b) c

Known [k] (Length k) (Ø k)

Known [k] (Length k) as => Known [k] (Length k) ((:<) k a as)

Known [k] (Prod k f) (Ø k)

Known (Maybe k) (Option k f) (Nothing k)

Known k f a => Known (Maybe k) (Option k f) (Just k a)

(Known k f a, Known [k] (Prod k f) as) => Known [k] (Prod k f) ((:<) k a as)

(Known k1 (p a) b, (~) ((,) k k1) q ((#) k k1 a b)) => Known ((,) k k) (Uncur k k p) q

((~) ((,) k k1) p ((#) k k1 a b), Known k f a, Known k1 g b) => Known ((,) k k) ((:*:) k k f g) p

Known k1 g b => Known (Either k k) ((:|:) k k f g) (Right k k b)

Known k1 f a => Known (Either k k) ((:|:) k k f g) (Left k k a)

(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

type WitnessC ØC (Known N Nat n) (Nat n) = ØC

type WitnessC ØC (Known N Nat n) (VT k n f a) = ØC