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.

Minimal complete definition

known

Associated Types

type KnownC f a :: Constraint

Methods

known :: f a

Instances

Known Bool Boolean False

Associated Types

type KnownC Boolean (False :: Boolean -> *) (a :: Boolean) :: Constraint

Methods

known :: False a

Known Bool Boolean True

Associated Types

type KnownC Boolean (True :: Boolean -> *) (a :: Boolean) :: Constraint

Methods

known :: True a

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.

Associated Types

type KnownC Wit (c :: Wit -> *) (a :: Wit) :: Constraint

Methods

known :: c a

Known N Nat Z

Z_ is the canonical construction of a Nat Z.

Associated Types

type KnownC Nat (Z :: Nat -> *) (a :: Nat) :: Constraint

Methods

known :: Z a

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

Associated Types

type KnownC Nat (S n :: Nat -> *) (a :: Nat) :: Constraint

Methods

known :: S n a

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

Associated Types

type KnownC ((:~:) k a) (b :: (:~:) k a -> *) (a :: (:~:) k a) :: Constraint

Methods

known :: b a

c a => Known k (Wit1 k c) a

Associated Types

type KnownC (Wit1 k c) (a :: Wit1 k c -> *) (a :: Wit1 k c) :: Constraint

Methods

known :: a a

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

Associated Types

type KnownC (Join k f) (a :: Join k f -> *) (a :: Join k f) :: Constraint

Methods

known :: a a

(∈) k a as => Known k (Index k as) a

Associated Types

type KnownC (Index k as) (a :: Index k as -> *) (a :: Index k as) :: Constraint

Methods

known :: a a

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

Associated Types

type KnownC (FProd k ((:<) (k -> *) f fs)) (a :: FProd k ((:<) (k -> *) f fs) -> *) (a :: FProd k ((:<) (k -> *) f fs)) :: Constraint

Methods

known :: a a

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

Associated Types

type KnownC (FProd k (Ø (k -> *))) (a :: FProd k (Ø (k -> *)) -> *) (a :: FProd k (Ø (k -> *))) :: Constraint

Methods

known :: a a

(~) N n (Len k as) => Witness ØC (Known N Nat n, Known [k] (Length k) as) (Length k as)

Associated Types

type WitnessC (ØC :: Constraint) ((Known N Nat n, Known [k] (Length k) as) :: Constraint) (Length k as) :: Constraint

Methods

(\\) :: ØC => ((Known N Nat n, Known [k] (Length k) as) -> r) -> Length k as -> r

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

Associated Types

type KnownC ((:&:) k f g) (a :: (:&:) k f g -> *) (a :: (:&:) k f g) :: Constraint

Methods

known :: a a

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

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

Associated Types

type WitnessC (ØC :: Constraint) (Known N Nat n :: Constraint) (Nat n) :: Constraint

Methods

(\\) :: ØC => (Known N Nat n -> r) -> Nat n -> r

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

Associated Types

type WitnessC (ØC :: Constraint) (Known N Nat n :: Constraint) (VecT k n f a) :: Constraint

Methods

(\\) :: ØC => (Known N Nat n -> r) -> VecT k n f a -> r

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

Associated Types

type KnownC (Cur k1 k p a) (b :: Cur k1 k p a -> *) (a :: Cur k1 k p a) :: Constraint

Methods

known :: b a

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

Associated Types

type KnownC (Flip k k1 p b) (a :: Flip k k1 p b -> *) (a :: Flip k k1 p b) :: Constraint

Methods

known :: a a

((~) 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)

Associated Types

type WitnessC (ØC :: Constraint) (((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) :: Constraint) (NatGT x y) :: Constraint

Methods

(\\) :: ØC => (((N ~ x) (S x'), Known N Nat y, (Bool ~ lt) False, (Bool ~ eq) False, (Bool ~ gt) True) -> r) -> NatGT x y -> r

((~) 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)

Associated Types

type WitnessC (ØC :: Constraint) (((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) :: Constraint) (NatEQ x y) :: Constraint

Methods

(\\) :: ØC => (((N ~ x) y, Known N Nat x, (Bool ~ lt) False, (Bool ~ eq) True, (Bool ~ gt) False) -> r) -> NatEQ x y -> r

((~) 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)

Associated Types

type WitnessC (ØC :: Constraint) (((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) :: Constraint) (NatLT x y) :: Constraint

Methods

(\\) :: ØC => (((N ~ y) (S y'), Known N Nat x, (Bool ~ lt) True, (Bool ~ eq) False, (Bool ~ gt) False) -> r) -> NatLT x y -> r

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

Associated Types

type KnownC (Cur3 k1 l k p a b) (c :: Cur3 k1 l k p a b -> *) (a :: Cur3 k1 l k p a b) :: Constraint

Methods

known :: c a

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

Associated Types

type KnownC (Length k) (Ø k :: Length k -> *) (a :: Length k) :: Constraint

Methods

known :: Ø k a

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

Associated Types

type KnownC (Length k) ((:<) k a as :: Length k -> *) (a :: Length k) :: Constraint

Methods

known :: (k :< a) as a

(Known [k] (Length k) as, Every k (Known k f) as) => Known [k] (Prod k f) as

Associated Types

type KnownC (Prod k f) (as :: Prod k f -> *) (a :: Prod k f) :: Constraint

Methods

known :: as a

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

Associated Types

type KnownC (Option k f) (Nothing k :: Option k f -> *) (a :: Option k f) :: Constraint

Methods

known :: Nothing k a

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

Associated Types

type KnownC (Option a f) (Just a a1 :: Option a f -> *) (a :: Option a f) :: Constraint

Methods

known :: Just a a1 a

Without k as a bs => Known [k] (Remove k as a) bs

Associated Types

type KnownC (Remove k as a) (bs :: Remove k as a -> *) (a :: Remove k as a) :: Constraint

Methods

known :: bs a

WithoutAll k as bs cs => Known [k] (Difference k as bs) cs

Associated Types

type KnownC (Difference k as bs) (cs :: Difference k as bs -> *) (a :: Difference k as bs) :: Constraint

Methods

known :: cs a

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

Associated Types

type KnownC (Uncur l k p) (q :: Uncur l k p -> *) (a :: Uncur l k p) :: Constraint

Methods

known :: q a

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

Associated Types

type KnownC ((:*:) l k f g) (p :: (:*:) l k f g -> *) (a :: (:*:) l k f g) :: Constraint

Methods

known :: p a

Known b g b1 => Known (Either k b) ((:+:) b k f g) (Right k b b1)

Associated Types

type KnownC ((:+:) b k f g) (Right k b b1 :: (:+:) b k f g -> *) (a :: (:+:) b k f g) :: Constraint

Methods

known :: Right k b b1 a

Known a f a1 => Known (Either a l) ((:+:) l a f g) (Left a l a1)

Associated Types

type KnownC ((:+:) l a f g) (Left a l a1 :: (:+:) l a f g -> *) (a :: (:+:) l a f g) :: Constraint

Methods

known :: Left a l a1 a

(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

Associated Types

type KnownC (Uncur3 m l k p) (q :: Uncur3 m l k p -> *) (a :: Uncur3 m l k p) :: Constraint

Methods

known :: q a

type WitnessC ØC (Known N Nat n, Known [k] (Length k) as) (Length k as)

type WitnessC ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) = (~) N n (Len k as)

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

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

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

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

type WitnessC ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y)

type WitnessC ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y) = ((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N x' (Pred x))

type WitnessC ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y)

type WitnessC ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y) = ((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y))

type WitnessC ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y)

type WitnessC ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y) = ((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N y' (Pred y))