Copyright | Copyright (C) 2015 Kyle Carter |
---|---|
License | BSD3 |
Maintainer | Kyle Carter <kylcarte@indiana.edu> |
Stability | experimental |
Portability | RankNTypes |
Safe Haskell | None |
Language | Haskell2010 |
Higher order analogs of type classes from the Prelude, and quantifier data types.
- class Eq1 f where
- (=#=) :: Eq1 f => f a -> f a -> Bool
- class Eq2 f where
- (=##=) :: Eq2 f => f a b -> f a b -> Bool
- class Eq3 f where
- (=###=) :: Eq3 f => f a b c -> f a b c -> Bool
- class Eq1 f => Ord1 f where
- class Eq2 f => Ord2 f where
- class Eq3 f => Ord3 f where
- class Show1 f where
- shows1 :: Show1 f => f a -> ShowS
- class Show2 f where
- shows2 :: Show2 f => f a b -> ShowS
- class Show3 f where
- shows3 :: Show3 f => f a b c -> ShowS
- class Read1 f where
- reads1 :: Read1 f => ReadS (Some f)
- readMaybe1 :: Read1 f => String -> Maybe (Some f)
- class Read2 f where
- reads2 :: Read2 f => ReadS (Some2 f)
- readMaybe2 :: Read2 f => String -> Maybe (Some2 f)
- class Read3 f where
- reads3 :: Read3 f => ReadS (Some3 f)
- readMaybe3 :: Read3 f => String -> Maybe (Some3 f)
- class Functor1 t where
- class IxFunctor1 i t | t -> i where
- class Foldable1 t where
- class IxFoldable1 i t | t -> i where
- class (Functor1 t, Foldable1 t) => Traversable1 t where
- class (IxFunctor1 i t, IxFoldable1 i t) => IxTraversable1 i t | t -> i where
- class Bifunctor1 t where
- class IxBifunctor1 i j t | t -> i j where
- data Some f :: * where
- some :: Some f -> (forall a. f a -> r) -> r
- (>>-) :: Some f -> (forall a. f a -> r) -> r
- (>->) :: (forall x. f x -> Some g) -> (forall x. g x -> Some h) -> f a -> Some h
- withSome :: (forall a. f a -> r) -> Some f -> r
- onSome :: (forall a. f a -> g x) -> Some f -> Some g
- msome :: Monad m => f a -> m (Some f)
- (>>=-) :: Monad m => m (Some f) -> (forall a. f a -> m r) -> m r
- data Some2 f :: * where
- some2 :: Some2 f -> (forall a b. f a b -> r) -> r
- (>>--) :: Some2 f -> (forall a b. f a b -> r) -> r
- (>-->) :: (forall x y. f x y -> Some2 g) -> (forall x y. g x y -> Some2 h) -> f a b -> Some2 h
- withSome2 :: (forall a b. f a b -> r) -> Some2 f -> r
- onSome2 :: (forall a b. f a b -> g x y) -> Some2 f -> Some2 g
- msome2 :: Monad m => f a b -> m (Some2 f)
- (>>=--) :: Monad m => m (Some2 f) -> (forall a b. f a b -> m r) -> m r
- data Some3 f :: * where
- some3 :: Some3 f -> (forall a b c. f a b c -> r) -> r
- (>>---) :: Some3 f -> (forall a b c. f a b c -> r) -> r
- (>--->) :: (forall x y z. f x y z -> Some3 g) -> (forall x y z. g x y z -> Some3 h) -> f a b c -> Some3 h
- withSome3 :: (forall a b c. f a b c -> r) -> Some3 f -> r
- onSome3 :: (forall a b c. f a b c -> g x y z) -> Some3 f -> Some3 g
- msome3 :: Monad m => f a b c -> m (Some3 f)
- (>>=---) :: Monad m => m (Some3 f) -> (forall a b c. f a b c -> m r) -> m r
- data SomeC c f where
- someC :: SomeC c f -> (forall a. c a => f a -> r) -> r
- (>>~) :: SomeC c f -> (forall a. c a => f a -> r) -> r
- msomeC :: (Monad m, c a) => f a -> m (SomeC c f)
- (>>=~) :: Monad m => m (SomeC c f) -> (forall a. c a => f a -> m r) -> m r
Documentation
Eq1 Bool Boolean Source # | |
Eq1 N Nat Source # | |
Eq1 N Fin Source # | |
Eq1 N (IFin x) Source # | |
Eq2 k k f => Eq1 k (Join k f) Source # | |
Eq r => Eq1 k (C k r) Source # | |
Eq1 k (Index k as) Source # | |
(Eq1 k f, Eq1 k g) => Eq1 k ((:&:) k f g) Source # | |
(Eq1 k f, Eq1 k g) => Eq1 k ((:|:) k f g) Source # | |
Eq1 l f => Eq1 k ((:.:) k l f g) Source # | |
Eq1 [k] (Length k) Source # | |
Eq1 k f => Eq1 [k] (Sum k f) Source # | |
Eq1 k f => Eq1 [k] (Prod k f) Source # | |
Eq1 [k] (Remove k as a) Source # | |
(Eq1 k f, Eq1 l g) => Eq1 (Either k l) ((:+:) l k f g) Source # | |
(Eq1 k f, Eq1 l g) => Eq1 (k, l) ((:*:) l k f g) Source # | |
class Eq1 f => Ord1 f where Source #
compare1 :: f a -> f a -> Ordering Source #
compare1 :: Ord (f a) => f a -> f a -> Ordering Source #
(<#) :: f a -> f a -> Bool infix 4 Source #
(>#) :: f a -> f a -> Bool infix 4 Source #
Ord1 Bool Boolean Source # | |
Ord1 N Nat Source # | |
Ord1 N Fin Source # | |
Ord1 N (IFin x) Source # | |
Ord2 k k f => Ord1 k (Join k f) Source # | |
Ord r => Ord1 k (C k r) Source # | |
Ord1 k (Index k as) Source # | |
(Ord1 k f, Ord1 k g) => Ord1 k ((:&:) k f g) Source # | |
(Ord1 k f, Ord1 k g) => Ord1 k ((:|:) k f g) Source # | |
Ord1 l f => Ord1 k ((:.:) k l f g) Source # | |
Ord1 [k] (Length k) Source # | |
Ord1 k f => Ord1 [k] (Sum k f) Source # | |
Ord1 k f => Ord1 [k] (Prod k f) Source # | |
Ord1 [k] (Remove k as a) Source # | |
(Ord1 k f, Ord1 l g) => Ord1 (Either k l) ((:+:) l k f g) Source # | |
(Ord1 k f, Ord1 l g) => Ord1 (k, l) ((:*:) l k f g) Source # | |
Show1 Bool Boolean Source # | |
Show1 N Nat Source # | |
Show1 N Fin Source # | |
Show1 N (IFin x) Source # | |
Show2 k k f => Show1 k (Join k f) Source # | |
Show r => Show1 k (C k r) Source # | |
Show1 k (Index k as) Source # | |
(Show1 k f, Show1 k g) => Show1 k ((:&:) k f g) Source # | |
(Show1 k f, Show1 k g) => Show1 k ((:|:) k f g) Source # | |
Show1 l f => Show1 k ((:.:) k l f g) Source # | |
Show1 [k] (Length k) Source # | |
Show1 k f => Show1 [k] (Sum k f) Source # | |
Show1 k f => Show1 [k] (Prod k f) Source # | |
Show1 [k] (Remove k as a) Source # | |
(Show1 k f, Show1 l g) => Show1 (Either k l) ((:+:) l k f g) Source # | |
(Show1 k f, Show1 l g) => Show1 (k, l) ((:*:) l k f g) Source # | |
Read1 Bool Boolean Source # | |
Read1 N Nat Source # | |
Read1 N Fin Source # | |
Read r => Read1 k (C k r) Source # | |
(Read1 k f, Read1 k g) => Read1 k ((:|:) k f g) Source # | |
Read1 [k] (Length k) Source # | |
Read1 k f => Read1 [k] (Sum k f) Source # | |
Read1 k f => Read1 [k] (Prod k f) Source # | |
Read2 l k p => Read1 (k, l) (Uncur l k p) Source # | |
(Read1 k f, Read1 l g) => Read1 (Either k l) ((:+:) l k f g) Source # | |
Read3 m l k p => Read1 (k, l, m) (Uncur3 m l k p) Source # | |
class Functor1 t where Source #
map1 :: (forall a. f a -> g a) -> t f b -> t g b Source #
Take a natural transformation to a lifted natural transformation.
Functor1 l l ((:&:) l f) Source # | |
Functor1 l l ((:|:) l f) Source # | |
Functor1 l l (VecT l n) Source # | |
(Functor1 m l f, Functor1 l k g) => Functor1 m k (Comp1 (k -> *) m (l -> *) f g) Source # | |
Functor1 [k] k (Sum k) Source # | |
Functor1 [k] k (Prod k) Source # | |
Functor1 (Maybe k) k (Option k) Source # | We can take a natural transformation of |
Functor1 [(k1, k)] k (Env k k1 k2) Source # | |
Functor1 (Either k1 k) k ((:+:) k k1 f) Source # | |
Functor1 (k1, k) k ((:*:) k k1 f) Source # | |
class IxFunctor1 i t | t -> i where Source #
class Foldable1 t where Source #
Foldable1 l l ((:&:) l f) Source # | |
Foldable1 l l ((:|:) l f) Source # | |
Foldable1 l l (VecT l n) Source # | |
Foldable1 [k] k (Sum k) Source # | |
Foldable1 [k] k (Prod k) Source # | |
Foldable1 (Maybe k) k (Option k) Source # | |
Foldable1 (Either k1 k) k ((:+:) k k1 f) Source # | |
Foldable1 (k1, k) k ((:*:) k k1 f) Source # | |
class IxFoldable1 i t | t -> i where Source #
IxFoldable1 k [k] (Index k) (Sum k) Source # | |
IxFoldable1 k [k] (Index k) (Prod k) Source # | |
class (Functor1 t, Foldable1 t) => Traversable1 t where Source #
traverse1 :: Applicative h => (forall a. f a -> h (g a)) -> t f b -> h (t g b) Source #
Traversable1 l l ((:&:) l f) Source # | |
Traversable1 l l ((:|:) l f) Source # | |
Traversable1 l l (VecT l n) Source # | |
Traversable1 [k] k (Sum k) Source # | |
Traversable1 [k] k (Prod k) Source # | |
Traversable1 (Maybe k) k (Option k) Source # | |
Traversable1 (Either k1 k) k ((:+:) k k1 f) Source # | |
Traversable1 (k1, k) k ((:*:) k k1 f) Source # | |
class (IxFunctor1 i t, IxFoldable1 i t) => IxTraversable1 i t | t -> i where Source #
itraverse1 :: Applicative h => (forall a. i b a -> f a -> h (g a)) -> t f b -> h (t g b) Source #
IxTraversable1 k [k] (Index k) (Sum k) Source # | |
IxTraversable1 k [k] (Index k) (Prod k) Source # | |
class Bifunctor1 t where Source #
Bifunctor1 m m m ((:&:) m) Source # | |
Bifunctor1 m m m ((:|:) m) Source # | |
Bifunctor1 (Either k l) l k ((:+:) l k) Source # | |
Bifunctor1 (k, l) l k ((:*:) l k) Source # | |
class IxBifunctor1 i j t | t -> i j where Source #
some :: Some f -> (forall a. f a -> r) -> r Source #
An eliminator for a Some
type.
Consider this function akin to a Monadic bind, except instead of binding into a Monad with a sequent function, we're binding into the existential quantification with a universal eliminator function.
It serves as an explicit delimiter in a program of where the type index may be used and depended on, and where it may not.
NB: the result type of the eliminating function may
not refer to the universally quantified type index a
.
(>-->) :: (forall x y. f x y -> Some2 g) -> (forall x y. g x y -> Some2 h) -> f a b -> Some2 h infixr 1 Source #