singletons-2.4.1: A framework for generating singleton types

Copyright(C) 2016 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRichard Eisenberg (rae@cs.brynmawr.edu)
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Singletons.Prelude.Function

Contents

Description

Defines singleton versions of the definitions in Data.Function.

Because many of these definitions are produced by Template Haskell, it is not possible to create proper Haddock documentation. Please look up the corresponding operation in Data.Function. Also, please excuse the apparent repeated variable names. This is due to an interaction between Template Haskell and Haddock.

Synopsis

Prelude re-exports

type family Id (a :: a) :: a where ... Source #

Equations

Id x = x 

sId :: forall (t :: a). Sing t -> Sing (Apply IdSym0 t :: a) Source #

type family Const (a :: a) (a :: b) :: a where ... Source #

Equations

Const x _ = x 

sConst :: forall (t :: a) (t :: b). Sing t -> Sing t -> Sing (Apply (Apply ConstSym0 t) t :: a) Source #

type family ((a :: TyFun b c -> Type) :. (a :: TyFun a b -> Type)) (a :: a) :: c where ... Source #

Equations

(f :. g) a_6989586621679448640 = Apply (Apply (Apply (Apply Lambda_6989586621679448645Sym0 f) g) a_6989586621679448640) a_6989586621679448640 

(%.) :: forall (t :: TyFun b c -> Type) (t :: TyFun a b -> Type) (t :: a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply (.@#@$) t) t) t :: c) infixr 9 Source #

type family Flip (a :: TyFun a (TyFun b c -> Type) -> Type) (a :: b) (a :: a) :: c where ... Source #

Equations

Flip f x y = Apply (Apply f y) x 

sFlip :: forall (t :: TyFun a (TyFun b c -> Type) -> Type) (t :: b) (t :: a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FlipSym0 t) t) t :: c) Source #

type family (a :: TyFun a b -> Type) $ (a :: a) :: b where ... Source #

Equations

f $ x = Apply f x 

(%$) :: forall (t :: TyFun a b -> Type) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply ($@#@$) t) t :: b) infixr 0 Source #

Other combinators

type family (a :: a) & (a :: TyFun a b -> Type) :: b where ... Source #

Equations

x & f = Apply f x 

(%&) :: forall (t :: a) (t :: TyFun a b -> Type). Sing t -> Sing t -> Sing (Apply (Apply (&@#@$) t) t :: b) infixl 1 Source #

type family On (a :: TyFun b (TyFun b c -> Type) -> Type) (a :: TyFun a b -> Type) (a :: a) (a :: a) :: c where ... infixl 0 Source #

Equations

On ty f a_6989586621679824196 a_6989586621679824198 = Apply (Apply (Apply (Apply (Apply (Apply Lambda_6989586621679824204Sym0 ty) f) a_6989586621679824196) a_6989586621679824198) a_6989586621679824196) a_6989586621679824198 

sOn :: forall (t :: TyFun b (TyFun b c -> Type) -> Type) (t :: TyFun a b -> Type) (t :: a) (t :: a). Sing t -> Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply (Apply OnSym0 t) t) t) t :: c) infixl 0 Source #

Defunctionalization symbols

data IdSym0 (l :: TyFun a6989586621679448468 a6989586621679448468) Source #

Instances
SuppressUnusedWarnings (IdSym0 :: TyFun a6989586621679448468 a6989586621679448468 -> *) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply (IdSym0 :: TyFun a a -> *) (l :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply (IdSym0 :: TyFun a a -> *) (l :: a) = Id l

type IdSym1 (t :: a6989586621679448468) = Id t Source #

data ConstSym0 (l :: TyFun a6989586621679448466 (TyFun b6989586621679448467 a6989586621679448466 -> Type)) Source #

Instances
SuppressUnusedWarnings (ConstSym0 :: TyFun a6989586621679448466 (TyFun b6989586621679448467 a6989586621679448466 -> Type) -> *) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply (ConstSym0 :: TyFun a6989586621679448466 (TyFun b6989586621679448467 a6989586621679448466 -> Type) -> *) (l :: a6989586621679448466) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply (ConstSym0 :: TyFun a6989586621679448466 (TyFun b6989586621679448467 a6989586621679448466 -> Type) -> *) (l :: a6989586621679448466) = (ConstSym1 l :: TyFun b6989586621679448467 a6989586621679448466 -> *)

data ConstSym1 (l :: a6989586621679448466) (l :: TyFun b6989586621679448467 a6989586621679448466) Source #

Instances
SuppressUnusedWarnings (ConstSym1 :: a6989586621679448466 -> TyFun b6989586621679448467 a6989586621679448466 -> *) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply (ConstSym1 l1 :: TyFun b a -> *) (l2 :: b) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply (ConstSym1 l1 :: TyFun b a -> *) (l2 :: b) = Const l1 l2

type ConstSym2 (t :: a6989586621679448466) (t :: b6989586621679448467) = Const t t Source #

data (.@#@$) (l :: TyFun (TyFun b6989586621679448463 c6989586621679448464 -> Type) (TyFun (TyFun a6989586621679448465 b6989586621679448463 -> Type) (TyFun a6989586621679448465 c6989586621679448464 -> Type) -> Type)) Source #

Instances
SuppressUnusedWarnings ((.@#@$) :: TyFun (TyFun b6989586621679448463 c6989586621679448464 -> Type) (TyFun (TyFun a6989586621679448465 b6989586621679448463 -> Type) (TyFun a6989586621679448465 c6989586621679448464 -> Type) -> Type) -> *) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply ((.@#@$) :: TyFun (TyFun b6989586621679448463 c6989586621679448464 -> Type) (TyFun (TyFun a6989586621679448465 b6989586621679448463 -> Type) (TyFun a6989586621679448465 c6989586621679448464 -> Type) -> Type) -> *) (l :: TyFun b6989586621679448463 c6989586621679448464 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply ((.@#@$) :: TyFun (TyFun b6989586621679448463 c6989586621679448464 -> Type) (TyFun (TyFun a6989586621679448465 b6989586621679448463 -> Type) (TyFun a6989586621679448465 c6989586621679448464 -> Type) -> Type) -> *) (l :: TyFun b6989586621679448463 c6989586621679448464 -> Type) = ((.@#@$$) l :: TyFun (TyFun a6989586621679448465 b6989586621679448463 -> Type) (TyFun a6989586621679448465 c6989586621679448464 -> Type) -> *)

data (l :: TyFun b6989586621679448463 c6989586621679448464 -> Type) .@#@$$ (l :: TyFun (TyFun a6989586621679448465 b6989586621679448463 -> Type) (TyFun a6989586621679448465 c6989586621679448464 -> Type)) Source #

Instances
SuppressUnusedWarnings ((.@#@$$) :: (TyFun b6989586621679448463 c6989586621679448464 -> Type) -> TyFun (TyFun a6989586621679448465 b6989586621679448463 -> Type) (TyFun a6989586621679448465 c6989586621679448464 -> Type) -> *) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply ((.@#@$$) l1 :: TyFun (TyFun a6989586621679448465 b6989586621679448463 -> Type) (TyFun a6989586621679448465 c6989586621679448464 -> Type) -> *) (l2 :: TyFun a6989586621679448465 b6989586621679448463 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply ((.@#@$$) l1 :: TyFun (TyFun a6989586621679448465 b6989586621679448463 -> Type) (TyFun a6989586621679448465 c6989586621679448464 -> Type) -> *) (l2 :: TyFun a6989586621679448465 b6989586621679448463 -> Type) = l1 .@#@$$$ l2

data ((l :: TyFun b6989586621679448463 c6989586621679448464 -> Type) .@#@$$$ (l :: TyFun a6989586621679448465 b6989586621679448463 -> Type)) (l :: TyFun a6989586621679448465 c6989586621679448464) Source #

Instances
SuppressUnusedWarnings ((.@#@$$$) :: (TyFun b6989586621679448463 c6989586621679448464 -> Type) -> (TyFun a6989586621679448465 b6989586621679448463 -> Type) -> TyFun a6989586621679448465 c6989586621679448464 -> *) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply (l1 .@#@$$$ l2 :: TyFun a c -> *) (l3 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply (l1 .@#@$$$ l2 :: TyFun a c -> *) (l3 :: a) = (l1 :. l2) l3

type (.@#@$$$$) (t :: TyFun b6989586621679448463 c6989586621679448464 -> Type) (t :: TyFun a6989586621679448465 b6989586621679448463 -> Type) (t :: a6989586621679448465) = (:.) t t t Source #

data FlipSym0 (l :: TyFun (TyFun a6989586621679448460 (TyFun b6989586621679448461 c6989586621679448462 -> Type) -> Type) (TyFun b6989586621679448461 (TyFun a6989586621679448460 c6989586621679448462 -> Type) -> Type)) Source #

Instances
SuppressUnusedWarnings (FlipSym0 :: TyFun (TyFun a6989586621679448460 (TyFun b6989586621679448461 c6989586621679448462 -> Type) -> Type) (TyFun b6989586621679448461 (TyFun a6989586621679448460 c6989586621679448462 -> Type) -> Type) -> *) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply (FlipSym0 :: TyFun (TyFun a6989586621679448460 (TyFun b6989586621679448461 c6989586621679448462 -> Type) -> Type) (TyFun b6989586621679448461 (TyFun a6989586621679448460 c6989586621679448462 -> Type) -> Type) -> *) (l :: TyFun a6989586621679448460 (TyFun b6989586621679448461 c6989586621679448462 -> Type) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply (FlipSym0 :: TyFun (TyFun a6989586621679448460 (TyFun b6989586621679448461 c6989586621679448462 -> Type) -> Type) (TyFun b6989586621679448461 (TyFun a6989586621679448460 c6989586621679448462 -> Type) -> Type) -> *) (l :: TyFun a6989586621679448460 (TyFun b6989586621679448461 c6989586621679448462 -> Type) -> Type) = FlipSym1 l

data FlipSym1 (l :: TyFun a6989586621679448460 (TyFun b6989586621679448461 c6989586621679448462 -> Type) -> Type) (l :: TyFun b6989586621679448461 (TyFun a6989586621679448460 c6989586621679448462 -> Type)) Source #

Instances
SuppressUnusedWarnings (FlipSym1 :: (TyFun a6989586621679448460 (TyFun b6989586621679448461 c6989586621679448462 -> Type) -> Type) -> TyFun b6989586621679448461 (TyFun a6989586621679448460 c6989586621679448462 -> Type) -> *) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply (FlipSym1 l1 :: TyFun b6989586621679448461 (TyFun a6989586621679448460 c6989586621679448462 -> Type) -> *) (l2 :: b6989586621679448461) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply (FlipSym1 l1 :: TyFun b6989586621679448461 (TyFun a6989586621679448460 c6989586621679448462 -> Type) -> *) (l2 :: b6989586621679448461) = FlipSym2 l1 l2

data FlipSym2 (l :: TyFun a6989586621679448460 (TyFun b6989586621679448461 c6989586621679448462 -> Type) -> Type) (l :: b6989586621679448461) (l :: TyFun a6989586621679448460 c6989586621679448462) Source #

Instances
SuppressUnusedWarnings (FlipSym2 :: (TyFun a6989586621679448460 (TyFun b6989586621679448461 c6989586621679448462 -> Type) -> Type) -> b6989586621679448461 -> TyFun a6989586621679448460 c6989586621679448462 -> *) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply (FlipSym2 l1 l2 :: TyFun a c -> *) (l3 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply (FlipSym2 l1 l2 :: TyFun a c -> *) (l3 :: a) = Flip l1 l2 l3

type FlipSym3 (t :: TyFun a6989586621679448460 (TyFun b6989586621679448461 c6989586621679448462 -> Type) -> Type) (t :: b6989586621679448461) (t :: a6989586621679448460) = Flip t t t Source #

data ($@#@$) (l :: TyFun (TyFun a6989586621679448457 b6989586621679448458 -> Type) (TyFun a6989586621679448457 b6989586621679448458 -> Type)) Source #

Instances
SuppressUnusedWarnings (($@#@$) :: TyFun (TyFun a6989586621679448457 b6989586621679448458 -> Type) (TyFun a6989586621679448457 b6989586621679448458 -> Type) -> *) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply (($@#@$) :: TyFun (TyFun a6989586621679448457 b6989586621679448458 -> Type) (TyFun a6989586621679448457 b6989586621679448458 -> Type) -> *) (l :: TyFun a6989586621679448457 b6989586621679448458 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply (($@#@$) :: TyFun (TyFun a6989586621679448457 b6989586621679448458 -> Type) (TyFun a6989586621679448457 b6989586621679448458 -> Type) -> *) (l :: TyFun a6989586621679448457 b6989586621679448458 -> Type) = ($@#@$$) l

data (l :: TyFun a6989586621679448457 b6989586621679448458 -> Type) $@#@$$ (l :: TyFun a6989586621679448457 b6989586621679448458) Source #

Instances
SuppressUnusedWarnings (($@#@$$) :: (TyFun a6989586621679448457 b6989586621679448458 -> Type) -> TyFun a6989586621679448457 b6989586621679448458 -> *) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply (($@#@$$) l1 :: TyFun a b -> *) (l2 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Base

type Apply (($@#@$$) l1 :: TyFun a b -> *) (l2 :: a) = l1 $ l2

type ($@#@$$$) (t :: TyFun a6989586621679448457 b6989586621679448458 -> Type) (t :: a6989586621679448457) = ($) t t Source #

data (&@#@$) (l :: TyFun a6989586621679824150 (TyFun (TyFun a6989586621679824150 b6989586621679824151 -> Type) b6989586621679824151 -> Type)) Source #

Instances
SuppressUnusedWarnings ((&@#@$) :: TyFun a6989586621679824150 (TyFun (TyFun a6989586621679824150 b6989586621679824151 -> Type) b6989586621679824151 -> Type) -> *) Source # 
Instance details

Defined in Data.Singletons.Prelude.Function

type Apply ((&@#@$) :: TyFun a6989586621679824150 (TyFun (TyFun a6989586621679824150 b6989586621679824151 -> Type) b6989586621679824151 -> Type) -> *) (l :: a6989586621679824150) Source # 
Instance details

Defined in Data.Singletons.Prelude.Function

type Apply ((&@#@$) :: TyFun a6989586621679824150 (TyFun (TyFun a6989586621679824150 b6989586621679824151 -> Type) b6989586621679824151 -> Type) -> *) (l :: a6989586621679824150) = ((&@#@$$) l :: TyFun (TyFun a6989586621679824150 b6989586621679824151 -> Type) b6989586621679824151 -> *)

data (l :: a6989586621679824150) &@#@$$ (l :: TyFun (TyFun a6989586621679824150 b6989586621679824151 -> Type) b6989586621679824151) Source #

Instances
SuppressUnusedWarnings ((&@#@$$) :: a6989586621679824150 -> TyFun (TyFun a6989586621679824150 b6989586621679824151 -> Type) b6989586621679824151 -> *) Source # 
Instance details

Defined in Data.Singletons.Prelude.Function

type Apply ((&@#@$$) l1 :: TyFun (TyFun a b -> Type) b -> *) (l2 :: TyFun a b -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Function

type Apply ((&@#@$$) l1 :: TyFun (TyFun a b -> Type) b -> *) (l2 :: TyFun a b -> Type) = l1 & l2

type (&@#@$$$) (t :: a6989586621679824150) (t :: TyFun a6989586621679824150 b6989586621679824151 -> Type) = (&) t t Source #

data OnSym0 (l :: TyFun (TyFun b6989586621679824152 (TyFun b6989586621679824152 c6989586621679824153 -> Type) -> Type) (TyFun (TyFun a6989586621679824154 b6989586621679824152 -> Type) (TyFun a6989586621679824154 (TyFun a6989586621679824154 c6989586621679824153 -> Type) -> Type) -> Type)) Source #

Instances
SuppressUnusedWarnings (OnSym0 :: TyFun (TyFun b6989586621679824152 (TyFun b6989586621679824152 c6989586621679824153 -> Type) -> Type) (TyFun (TyFun a6989586621679824154 b6989586621679824152 -> Type) (TyFun a6989586621679824154 (TyFun a6989586621679824154 c6989586621679824153 -> Type) -> Type) -> Type) -> *) Source # 
Instance details

Defined in Data.Singletons.Prelude.Function

type Apply (OnSym0 :: TyFun (TyFun b6989586621679824152 (TyFun b6989586621679824152 c6989586621679824153 -> Type) -> Type) (TyFun (TyFun a6989586621679824154 b6989586621679824152 -> Type) (TyFun a6989586621679824154 (TyFun a6989586621679824154 c6989586621679824153 -> Type) -> Type) -> Type) -> *) (l :: TyFun b6989586621679824152 (TyFun b6989586621679824152 c6989586621679824153 -> Type) -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Function

type Apply (OnSym0 :: TyFun (TyFun b6989586621679824152 (TyFun b6989586621679824152 c6989586621679824153 -> Type) -> Type) (TyFun (TyFun a6989586621679824154 b6989586621679824152 -> Type) (TyFun a6989586621679824154 (TyFun a6989586621679824154 c6989586621679824153 -> Type) -> Type) -> Type) -> *) (l :: TyFun b6989586621679824152 (TyFun b6989586621679824152 c6989586621679824153 -> Type) -> Type) = (OnSym1 l :: TyFun (TyFun a6989586621679824154 b6989586621679824152 -> Type) (TyFun a6989586621679824154 (TyFun a6989586621679824154 c6989586621679824153 -> Type) -> Type) -> *)

data OnSym1 (l :: TyFun b6989586621679824152 (TyFun b6989586621679824152 c6989586621679824153 -> Type) -> Type) (l :: TyFun (TyFun a6989586621679824154 b6989586621679824152 -> Type) (TyFun a6989586621679824154 (TyFun a6989586621679824154 c6989586621679824153 -> Type) -> Type)) Source #

Instances
SuppressUnusedWarnings (OnSym1 :: (TyFun b6989586621679824152 (TyFun b6989586621679824152 c6989586621679824153 -> Type) -> Type) -> TyFun (TyFun a6989586621679824154 b6989586621679824152 -> Type) (TyFun a6989586621679824154 (TyFun a6989586621679824154 c6989586621679824153 -> Type) -> Type) -> *) Source # 
Instance details

Defined in Data.Singletons.Prelude.Function

type Apply (OnSym1 l1 :: TyFun (TyFun a6989586621679824154 b6989586621679824152 -> Type) (TyFun a6989586621679824154 (TyFun a6989586621679824154 c6989586621679824153 -> Type) -> Type) -> *) (l2 :: TyFun a6989586621679824154 b6989586621679824152 -> Type) Source # 
Instance details

Defined in Data.Singletons.Prelude.Function

type Apply (OnSym1 l1 :: TyFun (TyFun a6989586621679824154 b6989586621679824152 -> Type) (TyFun a6989586621679824154 (TyFun a6989586621679824154 c6989586621679824153 -> Type) -> Type) -> *) (l2 :: TyFun a6989586621679824154 b6989586621679824152 -> Type) = OnSym2 l1 l2

data OnSym2 (l :: TyFun b6989586621679824152 (TyFun b6989586621679824152 c6989586621679824153 -> Type) -> Type) (l :: TyFun a6989586621679824154 b6989586621679824152 -> Type) (l :: TyFun a6989586621679824154 (TyFun a6989586621679824154 c6989586621679824153 -> Type)) Source #

Instances
SuppressUnusedWarnings (OnSym2 :: (TyFun b6989586621679824152 (TyFun b6989586621679824152 c6989586621679824153 -> Type) -> Type) -> (TyFun a6989586621679824154 b6989586621679824152 -> Type) -> TyFun a6989586621679824154 (TyFun a6989586621679824154 c6989586621679824153 -> Type) -> *) Source # 
Instance details

Defined in Data.Singletons.Prelude.Function

type Apply (OnSym2 l1 l2 :: TyFun a6989586621679824154 (TyFun a6989586621679824154 c6989586621679824153 -> Type) -> *) (l3 :: a6989586621679824154) Source # 
Instance details

Defined in Data.Singletons.Prelude.Function

type Apply (OnSym2 l1 l2 :: TyFun a6989586621679824154 (TyFun a6989586621679824154 c6989586621679824153 -> Type) -> *) (l3 :: a6989586621679824154) = OnSym3 l1 l2 l3

data OnSym3 (l :: TyFun b6989586621679824152 (TyFun b6989586621679824152 c6989586621679824153 -> Type) -> Type) (l :: TyFun a6989586621679824154 b6989586621679824152 -> Type) (l :: a6989586621679824154) (l :: TyFun a6989586621679824154 c6989586621679824153) Source #

Instances
SuppressUnusedWarnings (OnSym3 :: (TyFun b6989586621679824152 (TyFun b6989586621679824152 c6989586621679824153 -> Type) -> Type) -> (TyFun a6989586621679824154 b6989586621679824152 -> Type) -> a6989586621679824154 -> TyFun a6989586621679824154 c6989586621679824153 -> *) Source # 
Instance details

Defined in Data.Singletons.Prelude.Function

type Apply (OnSym3 l1 l2 l3 :: TyFun a c -> *) (l4 :: a) Source # 
Instance details

Defined in Data.Singletons.Prelude.Function

type Apply (OnSym3 l1 l2 l3 :: TyFun a c -> *) (l4 :: a) = On l1 l2 l3 l4

type OnSym4 (t :: TyFun b6989586621679824152 (TyFun b6989586621679824152 c6989586621679824153 -> Type) -> Type) (t :: TyFun a6989586621679824154 b6989586621679824152 -> Type) (t :: a6989586621679824154) (t :: a6989586621679824154) = On t t t t Source #