Copyright	Copyright (C) 2015 Kyle Carter
License	BSD3
Maintainer	Kyle Carter <kylcarte@indiana.edu>
Stability	experimental
Portability	RankNTypes
Safe Haskell	None
Language	Haskell2010

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

Known Bool Boolean False Source #
Associated Types type KnownC Boolean (False :: Boolean -> *) (a :: Boolean) :: Constraint Source # Methods known :: False a Source #
Known Bool Boolean True Source #
Associated Types type KnownC Boolean (True :: Boolean -> *) (a :: Boolean) :: Constraint Source # Methods known :: True a Source #
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 Types type KnownC Wit (c :: Wit -> *) (a :: Wit) :: Constraint Source # Methods known :: c a Source #
Known N Nat Z Source #	`Z_` is the canonical construction of a `Nat Z`.
Associated Types type KnownC Nat (Z :: Nat -> *) (a :: Nat) :: Constraint Source # Methods known :: Z a Source #
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 Types type KnownC Nat (S n :: Nat -> *) (a :: Nat) :: Constraint Source # Methods known :: S n a Source #
(~) k a b => Known k ((:~:) k a) b Source #
Associated Types type KnownC ((:~:) k a) (b :: (:~:) k a -> *) (a :: (:~:) k a) :: Constraint Source # Methods known :: b a Source #
c a => Known k (Wit1 k c) a Source #
Associated Types type KnownC (Wit1 k c) (a :: Wit1 k c -> *) (a :: Wit1 k c) :: Constraint Source # Methods known :: a a Source #
Known k (f a) a => Known k (Join k f) a Source #
Associated Types type KnownC (Join k f) (a :: Join k f -> *) (a :: Join k f) :: Constraint Source # Methods known :: a a Source #
(∈) k a as => Known k (Index k as) a Source #
Associated Types type KnownC (Index k as) (a :: Index k as -> *) (a :: Index k as) :: Constraint Source # Methods known :: a a Source #
(Known k f a, Known k (FProd k fs) a) => Known k (FProd k ((:<) (k -> *) f fs)) a Source #
Associated Types type KnownC (FProd k ((:<) (k -> ) f fs)) (a :: FProd k ((:<) (k -> ) f fs) -> ) (a :: FProd k ((:<) (k -> ) f fs)) :: Constraint Source # Methods known :: a a Source #
Known k (FProd k (Ø (k -> *))) a Source #
Associated Types type KnownC (FProd k (Ø (k -> ))) (a :: FProd k (Ø (k -> )) -> ) (a :: FProd k (Ø (k -> ))) :: Constraint Source # Methods known :: a a Source #
(~) N n (Len k as) => Witness ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) Source #
Associated Types type 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 Types type KnownC ((:&:) k f g) (a :: (:&:) k f g -> *) (a :: (:&:) k f g) :: Constraint Source # Methods known :: 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 Types type 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 Types type 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 Types type KnownC (Cur k1 k p a) (b :: Cur k1 k p a -> *) (a :: Cur k1 k p a) :: Constraint Source # Methods known :: b a Source #
Known k1 (p a) b => Known k (Flip k k1 p b) a Source #
Associated Types type KnownC (Flip k k1 p b) (a :: Flip k k1 p b -> *) (a :: Flip k k1 p b) :: Constraint Source # Methods known :: 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 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 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 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 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 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 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 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 Source # Methods known :: c a Source #
Known [k] (Length k) (Ø k) Source #
Associated Types type KnownC (Length k) (Ø k :: Length k -> *) (a :: Length k) :: Constraint Source # Methods known :: Ø k a Source #
Known [k] (Length k) as => Known [k] (Length k) ((:<) k a as) Source #
Associated Types type KnownC (Length k) ((:<) k a as :: Length k -> *) (a :: Length k) :: Constraint Source # Methods known :: (k :< a) as a Source #
(Known [k] (Length k) as, Every k (Known k f) as) => Known [k] (Prod k f) as Source #
Associated Types type KnownC (Prod k f) (as :: Prod k f -> *) (a :: Prod k f) :: Constraint Source # Methods known :: as a Source #
Known (Maybe k) (Option k f) (Nothing k) Source #
Associated Types type KnownC (Option k f) (Nothing k :: Option k f -> *) (a :: Option k f) :: Constraint Source # Methods known :: Nothing k a Source #
Known a f a1 => Known (Maybe a) (Option a f) (Just a a1) Source #
Associated Types type KnownC (Option a f) (Just a a1 :: Option a f -> *) (a :: Option a f) :: Constraint Source # Methods known :: Just a a1 a Source #
Without k as a bs => Known [k] (Remove k as a) bs Source #
Associated Types type KnownC (Remove k as a) (bs :: Remove k as a -> *) (a :: Remove k as a) :: Constraint Source # Methods known :: bs a Source #
WithoutAll k as bs cs => Known [k] (Difference k as bs) cs Source #
Associated Types type KnownC (Difference k as bs) (cs :: Difference k as bs -> *) (a :: Difference k as bs) :: Constraint Source # Methods known :: 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 Types type KnownC (Uncur l k p) (q :: Uncur l k p -> *) (a :: Uncur l k p) :: Constraint Source # Methods known :: 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 Types type KnownC ((::) l k f g) (p :: (::) l k f g -> ) (a :: (::) l k f g) :: Constraint Source # Methods known :: p a Source #
Known b g b1 => Known (Either k b) ((:+:) b k f g) (Right k b b1) Source #
Associated Types type KnownC ((:+:) b k f g) (Right k b b1 :: (:+:) b k f g -> *) (a :: (:+:) b k f g) :: Constraint Source # Methods known :: Right k b b1 a Source #
Known a f a1 => Known (Either a l) ((:+:) l a f g) (Left a l a1) Source #
Associated Types type KnownC ((:+:) l a f g) (Left a l a1 :: (:+:) l a f g -> *) (a :: (:+:) l a f g) :: Constraint Source # Methods known :: 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 Types type KnownC (Uncur3 m l k p) (q :: Uncur3 m l k p -> *) (a :: Uncur3 m l k p) :: Constraint Source # Methods known :: 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))