Copyright	(C) 2018 Ryan Scott
License	BSD-style (see LICENSE)
Maintainer	Ryan Scott
Stability	experimental
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Functor.Singletons

Contents

Defunctionalization symbols
Orphan instances

Description

Defines the promoted and singled versions of the Functor type class.

Synopsis

class PFunctor f where
- type Fmap (arg :: (~>) a b) (arg :: f a) :: f b
- type (arg :: a) <$ (arg :: f b) :: f a
class SFunctor f where
- sFmap :: forall a b (t :: (~>) a b) (t :: f a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t :: f b)
- (%<$) :: forall a b (t :: a) (t :: f b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t :: f a)
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 :: (~>) ((~>) a b) ((~>) (f a) (f b))
data FmapSym1 (a6989586621679337015 :: (~>) a b) :: (~>) (f a) (f b)
type family FmapSym2 (a6989586621679337015 :: (~>) a b) (a6989586621679337016 :: f a) :: f b where ...
data (<$@#@$) :: (~>) a ((~>) (f b) (f a))
data (<$@#@$$) (a6989586621679337020 :: a) :: (~>) (f b) (f a)
type family (a6989586621679337020 :: a) <$@#@$$$ (a6989586621679337021 :: f b) :: f a where ...
data ($>@#@$) :: (~>) (f a) ((~>) b (f b))
data ($>@#@$$) (a6989586621679524000 :: f a) :: (~>) b (f b)
type family (a6989586621679524000 :: f a) $>@#@$$$ (a6989586621679524001 :: b) :: f b where ...
data (<$>@#@$) :: (~>) ((~>) a b) ((~>) (f a) (f b))
data (<$>@#@$$) (a6989586621679524018 :: (~>) a b) :: (~>) (f a) (f b)
type family (a6989586621679524018 :: (~>) a b) <$>@#@$$$ (a6989586621679524019 :: f a) :: f b where ...
data (<&>@#@$) :: (~>) (f a) ((~>) ((~>) a b) (f b))
data (<&>@#@$$) (a6989586621679524007 :: f a) :: (~>) ((~>) a b) (f b)
type family (a6989586621679524007 :: f a) <&>@#@$$$ (a6989586621679524008 :: (~>) a b) :: f b where ...
data VoidSym0 :: (~>) (f a) (f ())
type family VoidSym1 (a6989586621679523991 :: f a) :: f () where ...

Documentation

class PFunctor f Source #

Associated Types

type Fmap (arg :: (~>) a b) (arg :: f a) :: f b Source #

type (arg :: a) <$ (arg :: f b) :: f a infixl 4 Source #

type a <$ a = Apply (Apply TFHelper_6989586621679337024Sym0 a) a

Instances

Instances details

PFunctor Identity Source #
Instance details Defined in Data.Functor.Identity.Singletons Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor First Source #
Instance details Defined in Data.Monoid.Singletons Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor Last Source #
Instance details Defined in Data.Monoid.Singletons Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor Down Source #
Instance details Defined in Data.Functor.Singletons Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor First Source #
Instance details Defined in Data.Semigroup.Singletons Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor Last Source #
Instance details Defined in Data.Semigroup.Singletons Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor Max Source #
Instance details Defined in Data.Semigroup.Singletons Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor Min Source #
Instance details Defined in Data.Semigroup.Singletons Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor Dual Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor Product Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor Sum Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor NonEmpty Source #
Instance details Defined in Control.Monad.Singletons.Internal Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor Maybe Source #
Instance details Defined in Control.Monad.Singletons.Internal Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor [] Source #
Instance details Defined in Control.Monad.Singletons.Internal Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor (Either a) Source #
Instance details Defined in Control.Monad.Singletons.Internal Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor (Proxy :: Type -> Type) Source #
Instance details Defined in Data.Proxy.Singletons Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor (Arg a) Source #
Instance details Defined in Data.Semigroup.Singletons Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor ((,) a) Source #
Instance details Defined in Data.Functor.Singletons Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor (Const m :: Type -> Type) Source #
Instance details Defined in Data.Functor.Const.Singletons Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor (Product f g) Source #
Instance details Defined in Data.Functor.Product.Singletons Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor (Sum f g) Source #
Instance details Defined in Data.Functor.Sum.Singletons Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PFunctor (Compose f g) Source #
Instance details Defined in Data.Functor.Compose.Singletons Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #

class SFunctor f where Source #

Minimal complete definition

sFmap

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 #

default (%<$) :: forall a b (t :: a) (t :: f b). (Apply (Apply (<$@#@$) t) t :: f a) ~ Apply (Apply TFHelper_6989586621679337024Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t :: f a) Source #

Instances

Instances details

SFunctor Identity Source #
Instance details Defined in Data.Functor.Identity.Singletons Methods sFmap :: forall a b (t :: a ~> b) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: Identity b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
SFunctor First Source #
Instance details Defined in Data.Monoid.Singletons Methods sFmap :: forall a b (t :: a ~> b) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: First b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
SFunctor Last Source #
Instance details Defined in Data.Monoid.Singletons Methods sFmap :: forall a b (t :: a ~> b) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: Last b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
SFunctor Down Source #
Instance details Defined in Data.Functor.Singletons Methods sFmap :: forall a b (t :: a ~> b) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: Down b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
SFunctor First Source #
Instance details Defined in Data.Semigroup.Singletons Methods sFmap :: forall a b (t :: a ~> b) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: First b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
SFunctor Last Source #
Instance details Defined in Data.Semigroup.Singletons Methods sFmap :: forall a b (t :: a ~> b) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: Last b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
SFunctor Max Source #
Instance details Defined in Data.Semigroup.Singletons Methods sFmap :: forall a b (t :: a ~> b) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: Max b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
SFunctor Min Source #
Instance details Defined in Data.Semigroup.Singletons Methods sFmap :: forall a b (t :: a ~> b) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: Min b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
SFunctor Dual Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods sFmap :: forall a b (t :: a ~> b) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: Dual b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
SFunctor Product Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods sFmap :: forall a b (t :: a ~> b) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: Product b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
SFunctor Sum Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods sFmap :: forall a b (t :: a ~> b) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: Sum b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
SFunctor NonEmpty Source #
Instance details Defined in Control.Monad.Singletons.Internal Methods sFmap :: forall a b (t :: a ~> b) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: NonEmpty b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
SFunctor Maybe Source #
Instance details Defined in Control.Monad.Singletons.Internal Methods sFmap :: forall a b (t :: a ~> b) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: Maybe b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
SFunctor [] Source #
Instance details Defined in Control.Monad.Singletons.Internal Methods sFmap :: forall a b (t :: a ~> b) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: [b]). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
SFunctor (Either a) Source #
Instance details Defined in Control.Monad.Singletons.Internal Methods sFmap :: forall a0 b (t :: a0 ~> b) (t :: Either a a0). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a0 b (t :: a0) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
SFunctor (Proxy :: Type -> Type) Source #
Instance details Defined in Data.Proxy.Singletons Methods sFmap :: forall a b (t :: a ~> b) (t :: Proxy a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: Proxy b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
SFunctor (Arg a) Source #
Instance details Defined in Data.Semigroup.Singletons Methods sFmap :: forall a0 b (t :: a0 ~> b) (t :: Arg a a0). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a0 b (t :: a0) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
SFunctor ((,) a) Source #
Instance details Defined in Data.Functor.Singletons Methods sFmap :: forall a0 b (t :: a0 ~> b) (t :: (a, a0)). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a0 b (t :: a0) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
SFunctor (Const m :: Type -> Type) Source #
Instance details Defined in Data.Functor.Const.Singletons Methods sFmap :: forall a b (t :: a ~> b) (t :: Const m a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: Const m b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
(SFunctor f, SFunctor g) => SFunctor (Product f g) Source #
Instance details Defined in Data.Functor.Product.Singletons Methods sFmap :: forall a b (t :: a ~> b) (t :: Product f g a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: Product f g b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
(SFunctor f, SFunctor g) => SFunctor (Sum f g) Source #
Instance details Defined in Data.Functor.Sum.Singletons Methods sFmap :: forall a b (t :: a ~> b) (t :: Sum f g a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: Sum f g b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
(SFunctor f, SFunctor g) => SFunctor (Compose f g) Source #
Instance details Defined in Data.Functor.Compose.Singletons Methods sFmap :: forall a b (t :: a ~> b) (t :: Compose f g a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: Compose f g b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #

type family (a :: f a) $> (a :: b) :: f b where ... infixl 4 Source #

Equations

a_6989586621679523993 $> a_6989586621679523995 = Apply (Apply (Apply FlipSym0 (<$@#@$)) a_6989586621679523993) a_6989586621679523995

(%$>) :: 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 #

type family (a :: (~>) a b) <$> (a :: f a) :: f b where ... infixl 4 Source #

Equations

a_6989586621679524011 <$> a_6989586621679524013 = Apply (Apply FmapSym0 a_6989586621679524011) a_6989586621679524013

(%<$>) :: 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 #

type family (a :: f a) <&> (a :: (~>) a b) :: f b where ... infixl 1 Source #

Equations

as <&> f = Apply (Apply (<$>@#@$) f) as

(%<&>) :: 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

sVoid :: forall f a (t :: f a). SFunctor f => Sing t -> Sing (Apply VoidSym0 t :: f ()) Source #

Defunctionalization symbols

data FmapSym0 :: (~>) ((~>) a b) ((~>) (f a) (f b)) Source #

Instances

Instances details

SFunctor f => SingI (FmapSym0 :: TyFun (a ~> b) (f a ~> f b) -> Type) Source #
Instance details Defined in Control.Monad.Singletons.Internal Methods sing :: Sing FmapSym0
SuppressUnusedWarnings (FmapSym0 :: TyFun (a ~> b) (f a ~> f b) -> Type) Source #
Instance details Defined in Control.Monad.Singletons.Internal Methods suppressUnusedWarnings :: () #
type Apply (FmapSym0 :: TyFun (a ~> b) (f a ~> f b) -> Type) (a6989586621679337015 :: a ~> b) Source #
Instance details Defined in Control.Monad.Singletons.Internal type Apply (FmapSym0 :: TyFun (a ~> b) (f a ~> f b) -> Type) (a6989586621679337015 :: a ~> b) = FmapSym1 a6989586621679337015 :: TyFun (f a) (f b) -> Type

data FmapSym1 (a6989586621679337015 :: (~>) a b) :: (~>) (f a) (f b) Source #

Instances

Instances details

SFunctor f => SingI1 (FmapSym1 :: (a ~> b) -> TyFun (f a) (f b) -> Type) Source #
Instance details Defined in Control.Monad.Singletons.Internal Methods liftSing :: forall (x :: k1). Sing x -> Sing (FmapSym1 x)
(SFunctor f, SingI d) => SingI (FmapSym1 d :: TyFun (f a) (f b) -> Type) Source #
Instance details Defined in Control.Monad.Singletons.Internal Methods sing :: Sing (FmapSym1 d)
SuppressUnusedWarnings (FmapSym1 a6989586621679337015 :: TyFun (f a) (f b) -> Type) Source #
Instance details Defined in Control.Monad.Singletons.Internal Methods suppressUnusedWarnings :: () #
type Apply (FmapSym1 a6989586621679337015 :: TyFun (f a) (f b) -> Type) (a6989586621679337016 :: f a) Source #
Instance details Defined in Control.Monad.Singletons.Internal type Apply (FmapSym1 a6989586621679337015 :: TyFun (f a) (f b) -> Type) (a6989586621679337016 :: f a) = Fmap a6989586621679337015 a6989586621679337016

type family FmapSym2 (a6989586621679337015 :: (~>) a b) (a6989586621679337016 :: f a) :: f b where ... Source #

Equations

FmapSym2 a6989586621679337015 a6989586621679337016 = Fmap a6989586621679337015 a6989586621679337016

data (<$@#@$) :: (~>) a ((~>) (f b) (f a)) infixl 4 Source #

Instances

Instances details

SFunctor f => SingI ((<$@#@$) :: TyFun a (f b ~> f a) -> Type) Source #
Instance details Defined in Control.Monad.Singletons.Internal Methods sing :: Sing (<$@#@$)
SuppressUnusedWarnings ((<$@#@$) :: TyFun a (f b ~> f a) -> Type) Source #
Instance details Defined in Control.Monad.Singletons.Internal Methods suppressUnusedWarnings :: () #
type Apply ((<$@#@$) :: TyFun a (f b ~> f a) -> Type) (a6989586621679337020 :: a) Source #
Instance details Defined in Control.Monad.Singletons.Internal type Apply ((<$@#@$) :: TyFun a (f b ~> f a) -> Type) (a6989586621679337020 :: a) = (<$@#@$$) a6989586621679337020 :: TyFun (f b) (f a) -> Type

data (<$@#@$$) (a6989586621679337020 :: a) :: (~>) (f b) (f a) infixl 4 Source #

Instances

Instances details

SFunctor f => SingI1 ((<$@#@$$) :: a -> TyFun (f b) (f a) -> Type) Source #
Instance details Defined in Control.Monad.Singletons.Internal Methods liftSing :: forall (x :: k1). Sing x -> Sing ((<$@#@$$) x)
(SFunctor f, SingI d) => SingI ((<$@#@$$) d :: TyFun (f b) (f a) -> Type) Source #
Instance details Defined in Control.Monad.Singletons.Internal Methods sing :: Sing ((<$@#@$$) d)
SuppressUnusedWarnings ((<$@#@$$) a6989586621679337020 :: TyFun (f b) (f a) -> Type) Source #
Instance details Defined in Control.Monad.Singletons.Internal Methods suppressUnusedWarnings :: () #
type Apply ((<$@#@$$) a6989586621679337020 :: TyFun (f b) (f a) -> Type) (a6989586621679337021 :: f b) Source #
Instance details Defined in Control.Monad.Singletons.Internal type Apply ((<$@#@$$) a6989586621679337020 :: TyFun (f b) (f a) -> Type) (a6989586621679337021 :: f b) = a6989586621679337020 <$ a6989586621679337021

type family (a6989586621679337020 :: a) <$@#@$$$ (a6989586621679337021 :: f b) :: f a where ... infixl 4 Source #

Equations

a6989586621679337020 <$@#@$$$ a6989586621679337021 = (<$) a6989586621679337020 a6989586621679337021

data ($>@#@$) :: (~>) (f a) ((~>) b (f b)) infixl 4 Source #

Instances

Instances details

SFunctor f => SingI (($>@#@$) :: TyFun (f a) (b ~> f b) -> Type) Source #
Instance details Defined in Data.Functor.Singletons Methods sing :: Sing ($>@#@$)
SuppressUnusedWarnings (($>@#@$) :: TyFun (f a) (b ~> f b) -> Type) Source #
Instance details Defined in Data.Functor.Singletons Methods suppressUnusedWarnings :: () #
type Apply (($>@#@$) :: TyFun (f a) (b ~> f b) -> Type) (a6989586621679524000 :: f a) Source #
Instance details Defined in Data.Functor.Singletons type Apply (($>@#@$) :: TyFun (f a) (b ~> f b) -> Type) (a6989586621679524000 :: f a) = ($>@#@$$) a6989586621679524000 :: TyFun b (f b) -> Type

data ($>@#@$$) (a6989586621679524000 :: f a) :: (~>) b (f b) infixl 4 Source #

Instances

Instances details

SFunctor f => SingI1 (($>@#@$$) :: f a -> TyFun b (f b) -> Type) Source #
Instance details Defined in Data.Functor.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (($>@#@$$) x)
(SFunctor f, SingI d) => SingI (($>@#@$$) d :: TyFun b (f b) -> Type) Source #
Instance details Defined in Data.Functor.Singletons Methods sing :: Sing (($>@#@$$) d)
SuppressUnusedWarnings (($>@#@$$) a6989586621679524000 :: TyFun b (f b) -> Type) Source #
Instance details Defined in Data.Functor.Singletons Methods suppressUnusedWarnings :: () #
type Apply (($>@#@$$) a6989586621679524000 :: TyFun b (f b) -> Type) (a6989586621679524001 :: b) Source #
Instance details Defined in Data.Functor.Singletons type Apply (($>@#@$$) a6989586621679524000 :: TyFun b (f b) -> Type) (a6989586621679524001 :: b) = a6989586621679524000 $> a6989586621679524001

type family (a6989586621679524000 :: f a) $>@#@$$$ (a6989586621679524001 :: b) :: f b where ... infixl 4 Source #

Equations

a6989586621679524000 $>@#@$$$ a6989586621679524001 = ($>) a6989586621679524000 a6989586621679524001

data (<$>@#@$) :: (~>) ((~>) a b) ((~>) (f a) (f b)) infixl 4 Source #

Instances

Instances details

SFunctor f => SingI ((<$>@#@$) :: TyFun (a ~> b) (f a ~> f b) -> Type) Source #
Instance details Defined in Data.Functor.Singletons Methods sing :: Sing (<$>@#@$)
SuppressUnusedWarnings ((<$>@#@$) :: TyFun (a ~> b) (f a ~> f b) -> Type) Source #
Instance details Defined in Data.Functor.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((<$>@#@$) :: TyFun (a ~> b) (f a ~> f b) -> Type) (a6989586621679524018 :: a ~> b) Source #
Instance details Defined in Data.Functor.Singletons type Apply ((<$>@#@$) :: TyFun (a ~> b) (f a ~> f b) -> Type) (a6989586621679524018 :: a ~> b) = (<$>@#@$$) a6989586621679524018 :: TyFun (f a) (f b) -> Type

data (<$>@#@$$) (a6989586621679524018 :: (~>) a b) :: (~>) (f a) (f b) infixl 4 Source #

Instances

Instances details

SFunctor f => SingI1 ((<$>@#@$$) :: (a ~> b) -> TyFun (f a) (f b) -> Type) Source #
Instance details Defined in Data.Functor.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing ((<$>@#@$$) x)
(SFunctor f, SingI d) => SingI ((<$>@#@$$) d :: TyFun (f a) (f b) -> Type) Source #
Instance details Defined in Data.Functor.Singletons Methods sing :: Sing ((<$>@#@$$) d)
SuppressUnusedWarnings ((<$>@#@$$) a6989586621679524018 :: TyFun (f a) (f b) -> Type) Source #
Instance details Defined in Data.Functor.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((<$>@#@$$) a6989586621679524018 :: TyFun (f a) (f b) -> Type) (a6989586621679524019 :: f a) Source #
Instance details Defined in Data.Functor.Singletons type Apply ((<$>@#@$$) a6989586621679524018 :: TyFun (f a) (f b) -> Type) (a6989586621679524019 :: f a) = a6989586621679524018 <$> a6989586621679524019

type family (a6989586621679524018 :: (~>) a b) <$>@#@$$$ (a6989586621679524019 :: f a) :: f b where ... infixl 4 Source #

Equations

a6989586621679524018 <$>@#@$$$ a6989586621679524019 = (<$>) a6989586621679524018 a6989586621679524019

data (<&>@#@$) :: (~>) (f a) ((~>) ((~>) a b) (f b)) infixl 1 Source #

Instances

Instances details

SFunctor f => SingI ((<&>@#@$) :: TyFun (f a) ((a ~> b) ~> f b) -> Type) Source #
Instance details Defined in Data.Functor.Singletons Methods sing :: Sing (<&>@#@$)
SuppressUnusedWarnings ((<&>@#@$) :: TyFun (f a) ((a ~> b) ~> f b) -> Type) Source #
Instance details Defined in Data.Functor.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((<&>@#@$) :: TyFun (f a) ((a ~> b) ~> f b) -> Type) (a6989586621679524007 :: f a) Source #
Instance details Defined in Data.Functor.Singletons type Apply ((<&>@#@$) :: TyFun (f a) ((a ~> b) ~> f b) -> Type) (a6989586621679524007 :: f a) = (<&>@#@$$) a6989586621679524007 :: TyFun (a ~> b) (f b) -> Type

data (<&>@#@$$) (a6989586621679524007 :: f a) :: (~>) ((~>) a b) (f b) infixl 1 Source #

Instances

Instances details

SFunctor f => SingI1 ((<&>@#@$$) :: f a -> TyFun (a ~> b) (f b) -> Type) Source #
Instance details Defined in Data.Functor.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing ((<&>@#@$$) x)
(SFunctor f, SingI d) => SingI ((<&>@#@$$) d :: TyFun (a ~> b) (f b) -> Type) Source #
Instance details Defined in Data.Functor.Singletons Methods sing :: Sing ((<&>@#@$$) d)
SuppressUnusedWarnings ((<&>@#@$$) a6989586621679524007 :: TyFun (a ~> b) (f b) -> Type) Source #
Instance details Defined in Data.Functor.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((<&>@#@$$) a6989586621679524007 :: TyFun (a ~> b) (f b) -> Type) (a6989586621679524008 :: a ~> b) Source #
Instance details Defined in Data.Functor.Singletons type Apply ((<&>@#@$$) a6989586621679524007 :: TyFun (a ~> b) (f b) -> Type) (a6989586621679524008 :: a ~> b) = a6989586621679524007 <&> a6989586621679524008

type family (a6989586621679524007 :: f a) <&>@#@$$$ (a6989586621679524008 :: (~>) a b) :: f b where ... infixl 1 Source #

Equations

a6989586621679524007 <&>@#@$$$ a6989586621679524008 = (<&>) a6989586621679524007 a6989586621679524008

data VoidSym0 :: (~>) (f a) (f ()) Source #

Instances

Instances details

SFunctor f => SingI (VoidSym0 :: TyFun (f a) (f ()) -> Type) Source #
Instance details Defined in Data.Functor.Singletons Methods sing :: Sing VoidSym0
SuppressUnusedWarnings (VoidSym0 :: TyFun (f a) (f ()) -> Type) Source #
Instance details Defined in Data.Functor.Singletons Methods suppressUnusedWarnings :: () #
type Apply (VoidSym0 :: TyFun (f a) (f ()) -> Type) (a6989586621679523991 :: f a) Source #
Instance details Defined in Data.Functor.Singletons type Apply (VoidSym0 :: TyFun (f a) (f ()) -> Type) (a6989586621679523991 :: f a) = Void a6989586621679523991

type family VoidSym1 (a6989586621679523991 :: f a) :: f () where ... Source #

Equations

VoidSym1 a6989586621679523991 = Void a6989586621679523991

Orphan instances

PFunctor Down Source #
Instance details Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
SFunctor Down Source #
Instance details Methods sFmap :: forall a b (t :: a ~> b) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: Down b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
PFunctor ((,) a) Source #
Instance details Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
SFunctor ((,) a) Source #
Instance details Methods sFmap :: forall a0 b (t :: a0 ~> b) (t :: (a, a0)). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a0 b (t :: a0) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #