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.

Associated Types

type KnownC f a :: Constraint Source

Methods

known :: f a Source

Instances

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`.
Known N Nat Z Source	`Z_` is the canonical construction of a `Nat Z`.
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)`.
(~) 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 `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) 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