Copyright | (C) 2018 Ryan Scott |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Ryan Scott |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
Data.Singletons.Prelude.Functor
Description
Defines the promoted and singled versions of the Functor
type class.
Synopsis
- class PFunctor (f :: Type -> Type) where
- class SFunctor (f :: Type -> Type) where
- type family (a :: f a) $> (a :: b) :: f b where ...
- (%$>) :: forall f a b (t :: f a) (t :: b). SFunctor f => Sing t -> Sing t -> Sing (Apply (Apply ($>@#@$) t) t :: f b)
- type family (a :: (~>) a b) <$> (a :: f a) :: f b where ...
- (%<$>) :: forall a b f (t :: (~>) a b) (t :: f a). SFunctor f => Sing t -> Sing t -> Sing (Apply (Apply (<$>@#@$) t) t :: f b)
- type family (a :: f a) <&> (a :: (~>) a b) :: f b where ...
- (%<&>) :: forall f a b (t :: f a) (t :: (~>) a b). SFunctor f => Sing t -> Sing t -> Sing (Apply (Apply (<&>@#@$) t) t :: f b)
- type family Void (a :: f a) :: f () where ...
- sVoid :: forall f a (t :: f a). SFunctor f => Sing t -> Sing (Apply VoidSym0 t :: f ())
- data FmapSym0 :: forall a6989586621679566897 b6989586621679566898 f6989586621679566896. (~>) ((~>) a6989586621679566897 b6989586621679566898) ((~>) (f6989586621679566896 a6989586621679566897) (f6989586621679566896 b6989586621679566898))
- data FmapSym1 (arg6989586621679567288 :: (~>) a6989586621679566897 b6989586621679566898) :: forall f6989586621679566896. (~>) (f6989586621679566896 a6989586621679566897) (f6989586621679566896 b6989586621679566898)
- type FmapSym2 (arg6989586621679567288 :: (~>) a6989586621679566897 b6989586621679566898) (arg6989586621679567289 :: f6989586621679566896 a6989586621679566897) = Fmap arg6989586621679567288 arg6989586621679567289
- data (<$@#@$) :: forall a6989586621679566899 f6989586621679566896 b6989586621679566900. (~>) a6989586621679566899 ((~>) (f6989586621679566896 b6989586621679566900) (f6989586621679566896 a6989586621679566899))
- data (<$@#@$$) (arg6989586621679567292 :: a6989586621679566899) :: forall f6989586621679566896 b6989586621679566900. (~>) (f6989586621679566896 b6989586621679566900) (f6989586621679566896 a6989586621679566899)
- type (<$@#@$$$) (arg6989586621679567292 :: a6989586621679566899) (arg6989586621679567293 :: f6989586621679566896 b6989586621679566900) = (<$) arg6989586621679567292 arg6989586621679567293
- data ($>@#@$) :: forall f6989586621679737066 a6989586621679737067 b6989586621679737068. (~>) (f6989586621679737066 a6989586621679737067) ((~>) b6989586621679737068 (f6989586621679737066 b6989586621679737068))
- data ($>@#@$$) (a6989586621679737138 :: f6989586621679737066 a6989586621679737067) :: forall b6989586621679737068. (~>) b6989586621679737068 (f6989586621679737066 b6989586621679737068)
- type ($>@#@$$$) (a6989586621679737138 :: f6989586621679737066 a6989586621679737067) (a6989586621679737139 :: b6989586621679737068) = ($>) a6989586621679737138 a6989586621679737139
- data (<$>@#@$) :: forall a6989586621679737073 b6989586621679737074 f6989586621679737072. (~>) ((~>) a6989586621679737073 b6989586621679737074) ((~>) (f6989586621679737072 a6989586621679737073) (f6989586621679737072 b6989586621679737074))
- data (<$>@#@$$) (a6989586621679737154 :: (~>) a6989586621679737073 b6989586621679737074) :: forall f6989586621679737072. (~>) (f6989586621679737072 a6989586621679737073) (f6989586621679737072 b6989586621679737074)
- type (<$>@#@$$$) (a6989586621679737154 :: (~>) a6989586621679737073 b6989586621679737074) (a6989586621679737155 :: f6989586621679737072 a6989586621679737073) = (<$>) a6989586621679737154 a6989586621679737155
- data (<&>@#@$) :: forall f6989586621679737069 a6989586621679737070 b6989586621679737071. (~>) (f6989586621679737069 a6989586621679737070) ((~>) ((~>) a6989586621679737070 b6989586621679737071) (f6989586621679737069 b6989586621679737071))
- data (<&>@#@$$) (a6989586621679737144 :: f6989586621679737069 a6989586621679737070) :: forall b6989586621679737071. (~>) ((~>) a6989586621679737070 b6989586621679737071) (f6989586621679737069 b6989586621679737071)
- type (<&>@#@$$$) (a6989586621679737144 :: f6989586621679737069 a6989586621679737070) (a6989586621679737145 :: (~>) a6989586621679737070 b6989586621679737071) = (<&>) a6989586621679737144 a6989586621679737145
- data VoidSym0 :: forall f6989586621679737064 a6989586621679737065. (~>) (f6989586621679737064 a6989586621679737065) (f6989586621679737064 ())
- type VoidSym1 (a6989586621679737131 :: f6989586621679737064 a6989586621679737065) = Void a6989586621679737131
Documentation
class PFunctor (f :: Type -> Type) Source #
Instances
PFunctor [] Source # | |
PFunctor Maybe Source # | |
PFunctor NonEmpty Source # | |
PFunctor Down Source # | |
PFunctor Identity Source # | |
PFunctor First Source # | |
PFunctor Last Source # | |
PFunctor Max Source # | |
PFunctor Min Source # | |
PFunctor Option Source # | |
PFunctor Dual Source # | |
PFunctor Product Source # | |
PFunctor Sum Source # | |
PFunctor First Source # | |
PFunctor Last Source # | |
PFunctor (Either a) Source # | |
PFunctor ((,) a) Source # | |
PFunctor (Arg a) Source # | |
PFunctor (Const m :: Type -> Type) Source # | |
class SFunctor (f :: Type -> Type) where Source #
Minimal complete definition
Methods
sFmap :: forall a b (t :: (~>) a b) (t :: f a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t :: f b) Source #
(%<$) :: forall a b (t :: a) (t :: f b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t :: f a) infixl 4 Source #
Instances
SFunctor [] Source # | |
SFunctor Maybe Source # | |
SFunctor NonEmpty Source # | |
SFunctor Down Source # | |
SFunctor Identity Source # | |
SFunctor First Source # | |
SFunctor Last Source # | |
SFunctor Max Source # | |
SFunctor Min Source # | |
SFunctor Option Source # | |
SFunctor Dual Source # | |
SFunctor Product Source # | |
SFunctor Sum Source # | |
SFunctor First Source # | |
SFunctor Last Source # | |
SFunctor (Either a) Source # | |
SFunctor ((,) a) Source # | |
SFunctor (Arg a) Source # | |
SFunctor (Const m :: Type -> Type) Source # | |
(%$>) :: forall f a b (t :: f a) (t :: b). SFunctor f => Sing t -> Sing t -> Sing (Apply (Apply ($>@#@$) t) t :: f b) infixl 4 Source #
(%<$>) :: forall a b f (t :: (~>) a b) (t :: f a). SFunctor f => Sing t -> Sing t -> Sing (Apply (Apply (<$>@#@$) t) t :: f b) infixl 4 Source #
(%<&>) :: forall f a b (t :: f a) (t :: (~>) a b). SFunctor f => Sing t -> Sing t -> Sing (Apply (Apply (<&>@#@$) t) t :: f b) infixl 1 Source #
type family Void (a :: f a) :: f () where ... Source #
Equations
Void x = Apply (Apply (<$@#@$) Tuple0Sym0) x |
Defunctionalization symbols
data FmapSym0 :: forall a6989586621679566897 b6989586621679566898 f6989586621679566896. (~>) ((~>) a6989586621679566897 b6989586621679566898) ((~>) (f6989586621679566896 a6989586621679566897) (f6989586621679566896 b6989586621679566898)) Source #
Instances
SFunctor f => SingI (FmapSym0 :: TyFun (a ~> b) (f a ~> f b) -> Type) Source # | |
SuppressUnusedWarnings (FmapSym0 :: TyFun (a6989586621679566897 ~> b6989586621679566898) (f6989586621679566896 a6989586621679566897 ~> f6989586621679566896 b6989586621679566898) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () Source # | |
type Apply (FmapSym0 :: TyFun (a6989586621679566897 ~> b6989586621679566898) (f6989586621679566896 a6989586621679566897 ~> f6989586621679566896 b6989586621679566898) -> Type) (arg6989586621679567288 :: a6989586621679566897 ~> b6989586621679566898) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal type Apply (FmapSym0 :: TyFun (a6989586621679566897 ~> b6989586621679566898) (f6989586621679566896 a6989586621679566897 ~> f6989586621679566896 b6989586621679566898) -> Type) (arg6989586621679567288 :: a6989586621679566897 ~> b6989586621679566898) = FmapSym1 arg6989586621679567288 f6989586621679566896 :: TyFun (f6989586621679566896 a6989586621679566897) (f6989586621679566896 b6989586621679566898) -> Type |
data FmapSym1 (arg6989586621679567288 :: (~>) a6989586621679566897 b6989586621679566898) :: forall f6989586621679566896. (~>) (f6989586621679566896 a6989586621679566897) (f6989586621679566896 b6989586621679566898) Source #
Instances
(SFunctor f, SingI d) => SingI (FmapSym1 d f :: TyFun (f a) (f b) -> Type) Source # | |
SuppressUnusedWarnings (FmapSym1 arg6989586621679567288 f6989586621679566896 :: TyFun (f6989586621679566896 a6989586621679566897) (f6989586621679566896 b6989586621679566898) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () Source # | |
type Apply (FmapSym1 arg6989586621679567288 f :: TyFun (f a) (f b) -> Type) (arg6989586621679567289 :: f a) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal |
type FmapSym2 (arg6989586621679567288 :: (~>) a6989586621679566897 b6989586621679566898) (arg6989586621679567289 :: f6989586621679566896 a6989586621679566897) = Fmap arg6989586621679567288 arg6989586621679567289 Source #
data (<$@#@$) :: forall a6989586621679566899 f6989586621679566896 b6989586621679566900. (~>) a6989586621679566899 ((~>) (f6989586621679566896 b6989586621679566900) (f6989586621679566896 a6989586621679566899)) infixl 4 Source #
Instances
SFunctor f => SingI ((<$@#@$) :: TyFun a (f b ~> f a) -> Type) Source # | |
SuppressUnusedWarnings ((<$@#@$) :: TyFun a6989586621679566899 (f6989586621679566896 b6989586621679566900 ~> f6989586621679566896 a6989586621679566899) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () Source # | |
type Apply ((<$@#@$) :: TyFun a6989586621679566899 (f6989586621679566896 b6989586621679566900 ~> f6989586621679566896 a6989586621679566899) -> Type) (arg6989586621679567292 :: a6989586621679566899) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal type Apply ((<$@#@$) :: TyFun a6989586621679566899 (f6989586621679566896 b6989586621679566900 ~> f6989586621679566896 a6989586621679566899) -> Type) (arg6989586621679567292 :: a6989586621679566899) = (arg6989586621679567292 <$@#@$$ f6989586621679566896) b6989586621679566900 :: TyFun (f6989586621679566896 b6989586621679566900) (f6989586621679566896 a6989586621679566899) -> Type |
data (<$@#@$$) (arg6989586621679567292 :: a6989586621679566899) :: forall f6989586621679566896 b6989586621679566900. (~>) (f6989586621679566896 b6989586621679566900) (f6989586621679566896 a6989586621679566899) infixl 4 Source #
Instances
(SFunctor f, SingI d) => SingI ((d <$@#@$$ f) b :: TyFun (f b) (f a) -> Type) Source # | |
SuppressUnusedWarnings ((arg6989586621679567292 <$@#@$$ f6989586621679566896) b6989586621679566900 :: TyFun (f6989586621679566896 b6989586621679566900) (f6989586621679566896 a6989586621679566899) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal Methods suppressUnusedWarnings :: () Source # | |
type Apply ((arg6989586621679567292 <$@#@$$ f) b :: TyFun (f b) (f a) -> Type) (arg6989586621679567293 :: f b) Source # | |
Defined in Data.Singletons.Prelude.Monad.Internal |
type (<$@#@$$$) (arg6989586621679567292 :: a6989586621679566899) (arg6989586621679567293 :: f6989586621679566896 b6989586621679566900) = (<$) arg6989586621679567292 arg6989586621679567293 Source #
data ($>@#@$) :: forall f6989586621679737066 a6989586621679737067 b6989586621679737068. (~>) (f6989586621679737066 a6989586621679737067) ((~>) b6989586621679737068 (f6989586621679737066 b6989586621679737068)) infixl 4 Source #
Instances
SFunctor f => SingI (($>@#@$) :: TyFun (f a) (b ~> f b) -> Type) Source # | |
SuppressUnusedWarnings (($>@#@$) :: TyFun (f6989586621679737066 a6989586621679737067) (b6989586621679737068 ~> f6989586621679737066 b6989586621679737068) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Functor Methods suppressUnusedWarnings :: () Source # | |
type Apply (($>@#@$) :: TyFun (f6989586621679737066 a6989586621679737067) (b6989586621679737068 ~> f6989586621679737066 b6989586621679737068) -> Type) (a6989586621679737138 :: f6989586621679737066 a6989586621679737067) Source # | |
Defined in Data.Singletons.Prelude.Functor type Apply (($>@#@$) :: TyFun (f6989586621679737066 a6989586621679737067) (b6989586621679737068 ~> f6989586621679737066 b6989586621679737068) -> Type) (a6989586621679737138 :: f6989586621679737066 a6989586621679737067) = a6989586621679737138 $>@#@$$ b6989586621679737068 :: TyFun b6989586621679737068 (f6989586621679737066 b6989586621679737068) -> Type |
data ($>@#@$$) (a6989586621679737138 :: f6989586621679737066 a6989586621679737067) :: forall b6989586621679737068. (~>) b6989586621679737068 (f6989586621679737066 b6989586621679737068) infixl 4 Source #
Instances
(SFunctor f, SingI d) => SingI (d $>@#@$$ b :: TyFun b (f b) -> Type) Source # | |
SuppressUnusedWarnings (a6989586621679737138 $>@#@$$ b6989586621679737068 :: TyFun b6989586621679737068 (f6989586621679737066 b6989586621679737068) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Functor Methods suppressUnusedWarnings :: () Source # | |
type Apply (a6989586621679737138 $>@#@$$ b :: TyFun b (f b) -> Type) (a6989586621679737139 :: b) Source # | |
Defined in Data.Singletons.Prelude.Functor |
type ($>@#@$$$) (a6989586621679737138 :: f6989586621679737066 a6989586621679737067) (a6989586621679737139 :: b6989586621679737068) = ($>) a6989586621679737138 a6989586621679737139 Source #
data (<$>@#@$) :: forall a6989586621679737073 b6989586621679737074 f6989586621679737072. (~>) ((~>) a6989586621679737073 b6989586621679737074) ((~>) (f6989586621679737072 a6989586621679737073) (f6989586621679737072 b6989586621679737074)) infixl 4 Source #
Instances
SFunctor f => SingI ((<$>@#@$) :: TyFun (a ~> b) (f a ~> f b) -> Type) Source # | |
SuppressUnusedWarnings ((<$>@#@$) :: TyFun (a6989586621679737073 ~> b6989586621679737074) (f6989586621679737072 a6989586621679737073 ~> f6989586621679737072 b6989586621679737074) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Functor Methods suppressUnusedWarnings :: () Source # | |
type Apply ((<$>@#@$) :: TyFun (a6989586621679737073 ~> b6989586621679737074) (f6989586621679737072 a6989586621679737073 ~> f6989586621679737072 b6989586621679737074) -> Type) (a6989586621679737154 :: a6989586621679737073 ~> b6989586621679737074) Source # | |
Defined in Data.Singletons.Prelude.Functor type Apply ((<$>@#@$) :: TyFun (a6989586621679737073 ~> b6989586621679737074) (f6989586621679737072 a6989586621679737073 ~> f6989586621679737072 b6989586621679737074) -> Type) (a6989586621679737154 :: a6989586621679737073 ~> b6989586621679737074) = a6989586621679737154 <$>@#@$$ f6989586621679737072 :: TyFun (f6989586621679737072 a6989586621679737073) (f6989586621679737072 b6989586621679737074) -> Type |
data (<$>@#@$$) (a6989586621679737154 :: (~>) a6989586621679737073 b6989586621679737074) :: forall f6989586621679737072. (~>) (f6989586621679737072 a6989586621679737073) (f6989586621679737072 b6989586621679737074) infixl 4 Source #
Instances
(SFunctor f, SingI d) => SingI (d <$>@#@$$ f :: TyFun (f a) (f b) -> Type) Source # | |
SuppressUnusedWarnings (a6989586621679737154 <$>@#@$$ f6989586621679737072 :: TyFun (f6989586621679737072 a6989586621679737073) (f6989586621679737072 b6989586621679737074) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Functor Methods suppressUnusedWarnings :: () Source # | |
type Apply (a6989586621679737154 <$>@#@$$ f :: TyFun (f a) (f b) -> Type) (a6989586621679737155 :: f a) Source # | |
Defined in Data.Singletons.Prelude.Functor |
type (<$>@#@$$$) (a6989586621679737154 :: (~>) a6989586621679737073 b6989586621679737074) (a6989586621679737155 :: f6989586621679737072 a6989586621679737073) = (<$>) a6989586621679737154 a6989586621679737155 Source #
data (<&>@#@$) :: forall f6989586621679737069 a6989586621679737070 b6989586621679737071. (~>) (f6989586621679737069 a6989586621679737070) ((~>) ((~>) a6989586621679737070 b6989586621679737071) (f6989586621679737069 b6989586621679737071)) infixl 1 Source #
Instances
SFunctor f => SingI ((<&>@#@$) :: TyFun (f a) ((a ~> b) ~> f b) -> Type) Source # | |
SuppressUnusedWarnings ((<&>@#@$) :: TyFun (f6989586621679737069 a6989586621679737070) ((a6989586621679737070 ~> b6989586621679737071) ~> f6989586621679737069 b6989586621679737071) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Functor Methods suppressUnusedWarnings :: () Source # | |
type Apply ((<&>@#@$) :: TyFun (f6989586621679737069 a6989586621679737070) ((a6989586621679737070 ~> b6989586621679737071) ~> f6989586621679737069 b6989586621679737071) -> Type) (a6989586621679737144 :: f6989586621679737069 a6989586621679737070) Source # | |
Defined in Data.Singletons.Prelude.Functor type Apply ((<&>@#@$) :: TyFun (f6989586621679737069 a6989586621679737070) ((a6989586621679737070 ~> b6989586621679737071) ~> f6989586621679737069 b6989586621679737071) -> Type) (a6989586621679737144 :: f6989586621679737069 a6989586621679737070) = a6989586621679737144 <&>@#@$$ b6989586621679737071 :: TyFun (a6989586621679737070 ~> b6989586621679737071) (f6989586621679737069 b6989586621679737071) -> Type |
data (<&>@#@$$) (a6989586621679737144 :: f6989586621679737069 a6989586621679737070) :: forall b6989586621679737071. (~>) ((~>) a6989586621679737070 b6989586621679737071) (f6989586621679737069 b6989586621679737071) infixl 1 Source #
Instances
(SFunctor f, SingI d) => SingI (d <&>@#@$$ b :: TyFun (a ~> b) (f b) -> Type) Source # | |
SuppressUnusedWarnings (a6989586621679737144 <&>@#@$$ b6989586621679737071 :: TyFun (a6989586621679737070 ~> b6989586621679737071) (f6989586621679737069 b6989586621679737071) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Functor Methods suppressUnusedWarnings :: () Source # | |
type Apply (a6989586621679737144 <&>@#@$$ b :: TyFun (a ~> b) (f b) -> Type) (a6989586621679737145 :: a ~> b) Source # | |
type (<&>@#@$$$) (a6989586621679737144 :: f6989586621679737069 a6989586621679737070) (a6989586621679737145 :: (~>) a6989586621679737070 b6989586621679737071) = (<&>) a6989586621679737144 a6989586621679737145 Source #
data VoidSym0 :: forall f6989586621679737064 a6989586621679737065. (~>) (f6989586621679737064 a6989586621679737065) (f6989586621679737064 ()) Source #
Instances
SFunctor f => SingI (VoidSym0 :: TyFun (f a) (f ()) -> Type) Source # | |
SuppressUnusedWarnings (VoidSym0 :: TyFun (f6989586621679737064 a6989586621679737065) (f6989586621679737064 ()) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Functor Methods suppressUnusedWarnings :: () Source # | |
type Apply (VoidSym0 :: TyFun (f a) (f ()) -> Type) (a6989586621679737131 :: f a) Source # | |
Defined in Data.Singletons.Prelude.Functor |
type VoidSym1 (a6989586621679737131 :: f6989586621679737064 a6989586621679737065) = Void a6989586621679737131 Source #