type-combinators-0.2.4.3: A collection of data types for type-level programming

Type.Class.Known

Description

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

Synopsis

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

Minimal complete definition

known

Associated Types

type KnownC f a :: Constraint Source #

Methods

known :: f a Source #

Instances

 Source # Associated Typestype KnownC Boolean (False :: Boolean -> *) (a :: Boolean) :: Constraint Source # Methods Source # Associated Typestype KnownC Boolean (True :: Boolean -> *) (a :: Boolean) :: Constraint Source # Methods c => Known Constraint Wit c Source # If the constraint c holds, there is a canonical construction for a term of type Wit c, viz. the constructor Wit. Associated Typestype KnownC Wit (c :: Wit -> *) (a :: Wit) :: Constraint Source # Methodsknown :: c a Source # Source # Z_ is the canonical construction of a Nat Z. Associated Typestype KnownC Nat (Z :: Nat -> *) (a :: Nat) :: Constraint Source # Methods Known N Nat n => Known N Nat (S n) Source # If n is a canonical construction of Nat n, S_ n is the canonical construction of Nat (S n). Associated Typestype KnownC Nat (S n :: Nat -> *) (a :: Nat) :: Constraint Source # Methodsknown :: S n a Source # (~) k a b => Known k ((:~:) k a) b Source # Associated Typestype KnownC ((:~:) k a) (b :: (:~:) k a -> *) (a :: (:~:) k a) :: Constraint Source # Methodsknown :: b a Source # c a => Known k (Wit1 k c) a Source # Associated Typestype KnownC (Wit1 k c) (a :: Wit1 k c -> *) (a :: Wit1 k c) :: Constraint Source # Methodsknown :: a a Source # Known k (f a) a => Known k (Join k f) a Source # Associated Typestype KnownC (Join k f) (a :: Join k f -> *) (a :: Join k f) :: Constraint Source # Methodsknown :: a a Source # (∈) k a as => Known k (Index k as) a Source # Associated Typestype KnownC (Index k as) (a :: Index k as -> *) (a :: Index k as) :: Constraint Source # Methodsknown :: a a Source # (Known k f a, Known k (FProd k fs) a) => Known k (FProd k ((:<) (k -> *) f fs)) a Source # Associated Typestype KnownC (FProd k ((:<) (k -> *) f fs)) (a :: FProd k ((:<) (k -> *) f fs) -> *) (a :: FProd k ((:<) (k -> *) f fs)) :: Constraint Source # Methodsknown :: a a Source # Known k (FProd k (Ø (k -> *))) a Source # Associated Typestype KnownC (FProd k (Ø (k -> *))) (a :: FProd k (Ø (k -> *)) -> *) (a :: FProd k (Ø (k -> *))) :: Constraint Source # Methodsknown :: a a Source # (~) N n (Len k as) => Witness ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) Source # Associated Typestype WitnessC (ØC :: Constraint) ((Known N Nat n, Known [k] (Length k) as) :: Constraint) (Length k as) :: Constraint Source # Methods(\\) :: ØC => ((Known N Nat n, Known [k] (Length k) as) -> r) -> Length k as -> r Source # (Known k f a, Known k g a) => Known k ((:&:) k f g) a Source # Associated Typestype KnownC ((:&:) k f g) (a :: (:&:) k f g -> *) (a :: (:&:) k f g) :: Constraint Source # Methodsknown :: a a Source # Witness ØC (Known N Nat n) (Nat n) Source # A Nat n is a Witness that there is a canonical construction for Nat n. Associated Typestype WitnessC (ØC :: Constraint) (Known N Nat n :: Constraint) (Nat n) :: Constraint Source # Methods(\\) :: ØC => (Known N Nat n -> r) -> Nat n -> r Source # Witness ØC (Known N Nat n) (VecT k n f a) Source # Associated Typestype WitnessC (ØC :: Constraint) (Known N Nat n :: Constraint) (VecT k n f a) :: Constraint Source # Methods(\\) :: ØC => (Known N Nat n -> r) -> VecT k n f a -> r Source # Known (k1, k) p ((#) k1 k a b) => Known k (Cur k1 k p a) b Source # Associated Typestype KnownC (Cur k1 k p a) (b :: Cur k1 k p a -> *) (a :: Cur k1 k p a) :: Constraint Source # Methodsknown :: b a Source # Known k1 (p a) b => Known k (Flip k k1 p b) a Source # Associated Typestype KnownC (Flip k k1 p b) (a :: Flip k k1 p b -> *) (a :: Flip k k1 p b) :: Constraint Source # Methodsknown :: a 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 # Associated Typestype 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 Source # Methods(\\) :: ØC => (((N ~ x) (S x'), Known N Nat y, (Bool ~ lt) False, (Bool ~ eq) False, (Bool ~ gt) True) -> r) -> NatGT x y -> r 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 # Associated Typestype WitnessC (ØC :: Constraint) (((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) :: Constraint) (NatEQ x y) :: Constraint Source # Methods(\\) :: ØC => (((N ~ x) y, Known N Nat x, (Bool ~ lt) False, (Bool ~ eq) True, (Bool ~ gt) False) -> r) -> NatEQ x y -> r 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 # Associated Typestype 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 Source # Methods(\\) :: ØC => (((N ~ y) (S y'), Known N Nat x, (Bool ~ lt) True, (Bool ~ eq) False, (Bool ~ gt) False) -> r) -> NatLT x y -> r Source # Known (k1, l, k) p ((,,) k1 l k a b c) => Known k (Cur3 k1 l k p a b) c Source # Associated Typestype 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 Source # Methodsknown :: c a Source # Known [k] (Length k) (Ø k) Source # Associated Typestype KnownC (Length k) (Ø k :: Length k -> *) (a :: Length k) :: Constraint Source # Methodsknown :: Ø k a Source # Known [k] (Length k) as => Known [k] (Length k) ((:<) k a as) Source # Associated Typestype KnownC (Length k) ((:<) k a as :: Length k -> *) (a :: Length k) :: Constraint Source # Methodsknown :: (k :< a) as a Source # (Known [k] (Length k) as, Every k (Known k f) as) => Known [k] (Prod k f) as Source # Associated Typestype KnownC (Prod k f) (as :: Prod k f -> *) (a :: Prod k f) :: Constraint Source # Methodsknown :: as a Source # Known (Maybe k) (Option k f) (Nothing k) Source # Associated Typestype KnownC (Option k f) (Nothing k :: Option k f -> *) (a :: Option k f) :: Constraint Source # Methodsknown :: Nothing k a Source # Known a f a1 => Known (Maybe a) (Option a f) (Just a a1) Source # Associated Typestype KnownC (Option a f) (Just a a1 :: Option a f -> *) (a :: Option a f) :: Constraint Source # Methodsknown :: Just a a1 a Source # Without k as a bs => Known [k] (Remove k as a) bs Source # Associated Typestype KnownC (Remove k as a) (bs :: Remove k as a -> *) (a :: Remove k as a) :: Constraint Source # Methodsknown :: bs a Source # WithoutAll k as bs cs => Known [k] (Difference k as bs) cs Source # Associated Typestype KnownC (Difference k as bs) (cs :: Difference k as bs -> *) (a :: Difference k as bs) :: Constraint Source # Methodsknown :: cs a Source # (Known l (p a) b, (~) (k, l) q ((#) k l a b)) => Known (k, l) (Uncur l k p) q Source # Associated Typestype KnownC (Uncur l k p) (q :: Uncur l k p -> *) (a :: Uncur l k p) :: Constraint Source # Methodsknown :: q a 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 # Associated Typestype KnownC ((:*:) l k f g) (p :: (:*:) l k f g -> *) (a :: (:*:) l k f g) :: Constraint Source # Methodsknown :: p a Source # Known b g b1 => Known (Either k b) ((:+:) b k f g) (Right k b b1) Source # Associated Typestype KnownC ((:+:) b k f g) (Right k b b1 :: (:+:) b k f g -> *) (a :: (:+:) b k f g) :: Constraint Source # Methodsknown :: Right k b b1 a Source # Known a f a1 => Known (Either a l) ((:+:) l a f g) (Left a l a1) Source # Associated Typestype KnownC ((:+:) l a f g) (Left a l a1 :: (:+:) l a f g -> *) (a :: (:+:) l a f g) :: Constraint Source # Methodsknown :: Left a l a1 a 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 # Associated Typestype KnownC (Uncur3 m l k p) (q :: Uncur3 m l k p -> *) (a :: Uncur3 m l k p) :: Constraint Source # Methodsknown :: q a Source # type WitnessC ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) Source # 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) Source # type WitnessC ØC (Known N Nat n) (Nat n) = ØC type WitnessC ØC (Known N Nat n) (VecT k n f a) Source # 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) Source # 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) Source # 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) Source # 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))