Copyright | Copyright (C) 2015 Kyle Carter |
---|---|

License | BSD3 |

Maintainer | Kyle Carter <kylcarte@indiana.edu> |

Stability | experimental |

Portability | RankNTypes |

Safe Haskell | None |

Language | Haskell2010 |

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

.

- class KnownC f a => Known f a where
- type KnownC f a :: Constraint

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

type KnownC f a :: Constraint Source #

Known Bool Boolean False Source # | |

Known Bool Boolean True Source # | |

c => Known Constraint Wit c Source # | If the constraint |

Known N Nat Z Source # | |

Known N Nat n => Known N Nat (S n) Source # | If |

(~) k a b => Known k ((:~:) k a) b Source # | |

c a => Known k (Wit1 k c) a Source # | |

Known k (f a) a => Known k (Join k f) a Source # | |

(∈) k a as => Known k (Index k as) a Source # | |

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

Known k (FProd k (Ø (k -> *))) a Source # | |

(~) N n (Len k as) => Witness ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) 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 |

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

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

Known k1 (p a) b => Known k (Flip k k1 p b) 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 # | |

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

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

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

Known [k] (Length k) (Ø k) Source # | |

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

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

Known (Maybe k) (Option k f) (Nothing k) Source # | |

Known a f a1 => Known (Maybe a) (Option a f) (Just a a1) Source # | |

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

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

(Known l (p a) b, (~) (k, l) q ((#) k l a b)) => Known (k, l) (Uncur l k p) q 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 # | |

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

Known a f a1 => Known (Either a l) ((:+:) l a f g) (Left a l a1) 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 # | |

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

type WitnessC ØC (Known N Nat n) (Nat n) Source # | |

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

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 y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ 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) Source # | |