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

Equations

Id x = x 

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

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

Equations

Const x _z_6989586621679244149 = x 

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

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

Equations

(f :. g) a_6989586621679244112 = Apply (Apply (Apply (Apply Lambda_6989586621679244117Sym0 f) g) a_6989586621679244112) a_6989586621679244112 

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

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

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

type family (f :: TyFun a b -> *) $ (x :: a) :: b infixr 0 #

Instances

type ($) k1 k f x # 
type ($) k1 k f x = (@@) k1 k f x

(%$) :: forall (f :: TyFun a b -> *) (x :: a). Sing f -> Sing x -> Sing ((($$) @@ f) @@ x) infixr 0 #

Other combinators

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

Equations

x :& f = Apply f x 

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

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

Equations

On ty f a_6989586621679253535 a_6989586621679253537 = Apply (Apply (Apply (Apply (Apply (Apply Lambda_6989586621679253543Sym0 ty) f) a_6989586621679253535) a_6989586621679253537) a_6989586621679253535) a_6989586621679253537 

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

Defunctionalization symbols

data IdSym0 (l :: TyFun a6989586621679244030 a6989586621679244030) #

Instances

SuppressUnusedWarnings (TyFun a6989586621679244030 a6989586621679244030 -> *) (IdSym0 a6989586621679244030) # 

Methods

suppressUnusedWarnings :: Proxy (IdSym0 a6989586621679244030) t -> () #

type Apply a a (IdSym0 a) l # 
type Apply a a (IdSym0 a) l = Id a l

type IdSym1 (t :: a6989586621679244030) = Id t #

data ConstSym0 (l :: TyFun a6989586621679244028 (TyFun b6989586621679244029 a6989586621679244028 -> Type)) #

Instances

SuppressUnusedWarnings (TyFun a6989586621679244028 (TyFun b6989586621679244029 a6989586621679244028 -> Type) -> *) (ConstSym0 b6989586621679244029 a6989586621679244028) # 

Methods

suppressUnusedWarnings :: Proxy (ConstSym0 b6989586621679244029 a6989586621679244028) t -> () #

type Apply a6989586621679244028 (TyFun b6989586621679244029 a6989586621679244028 -> Type) (ConstSym0 b6989586621679244029 a6989586621679244028) l # 
type Apply a6989586621679244028 (TyFun b6989586621679244029 a6989586621679244028 -> Type) (ConstSym0 b6989586621679244029 a6989586621679244028) l = ConstSym1 b6989586621679244029 a6989586621679244028 l

data ConstSym1 (l :: a6989586621679244028) (l :: TyFun b6989586621679244029 a6989586621679244028) #

Instances

SuppressUnusedWarnings (a6989586621679244028 -> TyFun b6989586621679244029 a6989586621679244028 -> *) (ConstSym1 b6989586621679244029 a6989586621679244028) # 

Methods

suppressUnusedWarnings :: Proxy (ConstSym1 b6989586621679244029 a6989586621679244028) t -> () #

type Apply b a (ConstSym1 b a l1) l2 # 
type Apply b a (ConstSym1 b a l1) l2 = Const b a l1 l2

type ConstSym2 (t :: a6989586621679244028) (t :: b6989586621679244029) = Const t t #

data (:.$) (l :: TyFun (TyFun b6989586621679244025 c6989586621679244026 -> Type) (TyFun (TyFun a6989586621679244027 b6989586621679244025 -> Type) (TyFun a6989586621679244027 c6989586621679244026 -> Type) -> Type)) #

Instances

SuppressUnusedWarnings (TyFun (TyFun b6989586621679244025 c6989586621679244026 -> Type) (TyFun (TyFun a6989586621679244027 b6989586621679244025 -> Type) (TyFun a6989586621679244027 c6989586621679244026 -> Type) -> Type) -> *) ((:.$) b6989586621679244025 a6989586621679244027 c6989586621679244026) # 

Methods

suppressUnusedWarnings :: Proxy ((b6989586621679244025 :.$ a6989586621679244027) c6989586621679244026) t -> () #

type Apply (TyFun b6989586621679244025 c6989586621679244026 -> Type) (TyFun (TyFun a6989586621679244027 b6989586621679244025 -> Type) (TyFun a6989586621679244027 c6989586621679244026 -> Type) -> Type) ((:.$) b6989586621679244025 a6989586621679244027 c6989586621679244026) l # 
type Apply (TyFun b6989586621679244025 c6989586621679244026 -> Type) (TyFun (TyFun a6989586621679244027 b6989586621679244025 -> Type) (TyFun a6989586621679244027 c6989586621679244026 -> Type) -> Type) ((:.$) b6989586621679244025 a6989586621679244027 c6989586621679244026) l = (:.$$) b6989586621679244025 a6989586621679244027 c6989586621679244026 l

data (l :: TyFun b6989586621679244025 c6989586621679244026 -> Type) :.$$ (l :: TyFun (TyFun a6989586621679244027 b6989586621679244025 -> Type) (TyFun a6989586621679244027 c6989586621679244026 -> Type)) #

Instances

SuppressUnusedWarnings ((TyFun b6989586621679244025 c6989586621679244026 -> Type) -> TyFun (TyFun a6989586621679244027 b6989586621679244025 -> Type) (TyFun a6989586621679244027 c6989586621679244026 -> Type) -> *) ((:.$$) b6989586621679244025 a6989586621679244027 c6989586621679244026) # 

Methods

suppressUnusedWarnings :: Proxy ((b6989586621679244025 :.$$ a6989586621679244027) c6989586621679244026) t -> () #

type Apply (TyFun a6989586621679244027 b6989586621679244025 -> Type) (TyFun a6989586621679244027 c6989586621679244026 -> Type) ((:.$$) b6989586621679244025 a6989586621679244027 c6989586621679244026 l1) l2 # 
type Apply (TyFun a6989586621679244027 b6989586621679244025 -> Type) (TyFun a6989586621679244027 c6989586621679244026 -> Type) ((:.$$) b6989586621679244025 a6989586621679244027 c6989586621679244026 l1) l2 = (:.$$$) b6989586621679244025 a6989586621679244027 c6989586621679244026 l1 l2

data ((l :: TyFun b6989586621679244025 c6989586621679244026 -> Type) :.$$$ (l :: TyFun a6989586621679244027 b6989586621679244025 -> Type)) (l :: TyFun a6989586621679244027 c6989586621679244026) #

Instances

SuppressUnusedWarnings ((TyFun b6989586621679244025 c6989586621679244026 -> Type) -> (TyFun a6989586621679244027 b6989586621679244025 -> Type) -> TyFun a6989586621679244027 c6989586621679244026 -> *) ((:.$$$) b6989586621679244025 a6989586621679244027 c6989586621679244026) # 

Methods

suppressUnusedWarnings :: Proxy ((b6989586621679244025 :.$$$ a6989586621679244027) c6989586621679244026) t -> () #

type Apply a c ((:.$$$) b a c l1 l2) l3 # 
type Apply a c ((:.$$$) b a c l1 l2) l3 = (:.) b a c l1 l2 l3

type (:.$$$$) (t :: TyFun b6989586621679244025 c6989586621679244026 -> Type) (t :: TyFun a6989586621679244027 b6989586621679244025 -> Type) (t :: a6989586621679244027) = (:.) t t t #

data FlipSym0 (l :: TyFun (TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) (TyFun b6989586621679244023 (TyFun a6989586621679244022 c6989586621679244024 -> Type) -> Type)) #

Instances

SuppressUnusedWarnings (TyFun (TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) (TyFun b6989586621679244023 (TyFun a6989586621679244022 c6989586621679244024 -> Type) -> Type) -> *) (FlipSym0 b6989586621679244023 a6989586621679244022 c6989586621679244024) # 

Methods

suppressUnusedWarnings :: Proxy (FlipSym0 b6989586621679244023 a6989586621679244022 c6989586621679244024) t -> () #

type Apply (TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) (TyFun b6989586621679244023 (TyFun a6989586621679244022 c6989586621679244024 -> Type) -> Type) (FlipSym0 b6989586621679244023 a6989586621679244022 c6989586621679244024) l # 
type Apply (TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) (TyFun b6989586621679244023 (TyFun a6989586621679244022 c6989586621679244024 -> Type) -> Type) (FlipSym0 b6989586621679244023 a6989586621679244022 c6989586621679244024) l = FlipSym1 b6989586621679244023 a6989586621679244022 c6989586621679244024 l

data FlipSym1 (l :: TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) (l :: TyFun b6989586621679244023 (TyFun a6989586621679244022 c6989586621679244024 -> Type)) #

Instances

SuppressUnusedWarnings ((TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) -> TyFun b6989586621679244023 (TyFun a6989586621679244022 c6989586621679244024 -> Type) -> *) (FlipSym1 b6989586621679244023 a6989586621679244022 c6989586621679244024) # 

Methods

suppressUnusedWarnings :: Proxy (FlipSym1 b6989586621679244023 a6989586621679244022 c6989586621679244024) t -> () #

type Apply b6989586621679244023 (TyFun a6989586621679244022 c6989586621679244024 -> Type) (FlipSym1 b6989586621679244023 a6989586621679244022 c6989586621679244024 l1) l2 # 
type Apply b6989586621679244023 (TyFun a6989586621679244022 c6989586621679244024 -> Type) (FlipSym1 b6989586621679244023 a6989586621679244022 c6989586621679244024 l1) l2 = FlipSym2 b6989586621679244023 a6989586621679244022 c6989586621679244024 l1 l2

data FlipSym2 (l :: TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) (l :: b6989586621679244023) (l :: TyFun a6989586621679244022 c6989586621679244024) #

Instances

SuppressUnusedWarnings ((TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) -> b6989586621679244023 -> TyFun a6989586621679244022 c6989586621679244024 -> *) (FlipSym2 b6989586621679244023 a6989586621679244022 c6989586621679244024) # 

Methods

suppressUnusedWarnings :: Proxy (FlipSym2 b6989586621679244023 a6989586621679244022 c6989586621679244024) t -> () #

type Apply a c (FlipSym2 b a c l1 l2) l3 # 
type Apply a c (FlipSym2 b a c l1 l2) l3 = Flip b a c l1 l2 l3

type FlipSym3 (t :: TyFun a6989586621679244022 (TyFun b6989586621679244023 c6989586621679244024 -> Type) -> Type) (t :: b6989586621679244023) (t :: a6989586621679244022) = Flip t t t #

data ($$) :: TyFun (TyFun a b -> *) (TyFun a b -> *) -> * #

Instances

type Apply (TyFun a b -> *) (TyFun a b -> *) (($$) a b) arg # 
type Apply (TyFun a b -> *) (TyFun a b -> *) (($$) a b) arg = ($$$) a b arg

data ($$$) :: (TyFun a b -> *) -> TyFun a b -> * #

Instances

type Apply a k (($$$) a k f) arg # 
type Apply a k (($$$) a k f) arg = ($$$$) a k f arg

type ($$$$) a b = ($) a b #

data (:&$) (l :: TyFun a6989586621679253489 (TyFun (TyFun a6989586621679253489 b6989586621679253490 -> Type) b6989586621679253490 -> Type)) #

Instances

SuppressUnusedWarnings (TyFun a6989586621679253489 (TyFun (TyFun a6989586621679253489 b6989586621679253490 -> Type) b6989586621679253490 -> Type) -> *) ((:&$) a6989586621679253489 b6989586621679253490) # 

Methods

suppressUnusedWarnings :: Proxy (a6989586621679253489 :&$ b6989586621679253490) t -> () #

type Apply a6989586621679253489 (TyFun (TyFun a6989586621679253489 b6989586621679253490 -> Type) b6989586621679253490 -> Type) ((:&$) a6989586621679253489 b6989586621679253490) l # 
type Apply a6989586621679253489 (TyFun (TyFun a6989586621679253489 b6989586621679253490 -> Type) b6989586621679253490 -> Type) ((:&$) a6989586621679253489 b6989586621679253490) l = (:&$$) a6989586621679253489 b6989586621679253490 l

data (l :: a6989586621679253489) :&$$ (l :: TyFun (TyFun a6989586621679253489 b6989586621679253490 -> Type) b6989586621679253490) #

Instances

SuppressUnusedWarnings (a6989586621679253489 -> TyFun (TyFun a6989586621679253489 b6989586621679253490 -> Type) b6989586621679253490 -> *) ((:&$$) a6989586621679253489 b6989586621679253490) # 

Methods

suppressUnusedWarnings :: Proxy (a6989586621679253489 :&$$ b6989586621679253490) t -> () #

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

type (:&$$$) (t :: a6989586621679253489) (t :: TyFun a6989586621679253489 b6989586621679253490 -> Type) = (:&) t t #

data OnSym0 (l :: TyFun (TyFun b6989586621679253491 (TyFun b6989586621679253491 c6989586621679253492 -> Type) -> Type) (TyFun (TyFun a6989586621679253493 b6989586621679253491 -> Type) (TyFun a6989586621679253493 (TyFun a6989586621679253493 c6989586621679253492 -> Type) -> Type) -> Type)) #

Instances

SuppressUnusedWarnings (TyFun (TyFun b6989586621679253491 (TyFun b6989586621679253491 c6989586621679253492 -> Type) -> Type) (TyFun (TyFun a6989586621679253493 b6989586621679253491 -> Type) (TyFun a6989586621679253493 (TyFun a6989586621679253493 c6989586621679253492 -> Type) -> Type) -> Type) -> *) (OnSym0 b6989586621679253491 a6989586621679253493 c6989586621679253492) # 

Methods

suppressUnusedWarnings :: Proxy (OnSym0 b6989586621679253491 a6989586621679253493 c6989586621679253492) t -> () #

type Apply (TyFun b6989586621679253491 (TyFun b6989586621679253491 c6989586621679253492 -> Type) -> Type) (TyFun (TyFun a6989586621679253493 b6989586621679253491 -> Type) (TyFun a6989586621679253493 (TyFun a6989586621679253493 c6989586621679253492 -> Type) -> Type) -> Type) (OnSym0 b6989586621679253491 a6989586621679253493 c6989586621679253492) l # 
type Apply (TyFun b6989586621679253491 (TyFun b6989586621679253491 c6989586621679253492 -> Type) -> Type) (TyFun (TyFun a6989586621679253493 b6989586621679253491 -> Type) (TyFun a6989586621679253493 (TyFun a6989586621679253493 c6989586621679253492 -> Type) -> Type) -> Type) (OnSym0 b6989586621679253491 a6989586621679253493 c6989586621679253492) l = OnSym1 b6989586621679253491 a6989586621679253493 c6989586621679253492 l

data OnSym1 (l :: TyFun b6989586621679253491 (TyFun b6989586621679253491 c6989586621679253492 -> Type) -> Type) (l :: TyFun (TyFun a6989586621679253493 b6989586621679253491 -> Type) (TyFun a6989586621679253493 (TyFun a6989586621679253493 c6989586621679253492 -> Type) -> Type)) #

Instances

SuppressUnusedWarnings ((TyFun b6989586621679253491 (TyFun b6989586621679253491 c6989586621679253492 -> Type) -> Type) -> TyFun (TyFun a6989586621679253493 b6989586621679253491 -> Type) (TyFun a6989586621679253493 (TyFun a6989586621679253493 c6989586621679253492 -> Type) -> Type) -> *) (OnSym1 b6989586621679253491 a6989586621679253493 c6989586621679253492) # 

Methods

suppressUnusedWarnings :: Proxy (OnSym1 b6989586621679253491 a6989586621679253493 c6989586621679253492) t -> () #

type Apply (TyFun a6989586621679253493 b6989586621679253491 -> Type) (TyFun a6989586621679253493 (TyFun a6989586621679253493 c6989586621679253492 -> Type) -> Type) (OnSym1 b6989586621679253491 a6989586621679253493 c6989586621679253492 l1) l2 # 
type Apply (TyFun a6989586621679253493 b6989586621679253491 -> Type) (TyFun a6989586621679253493 (TyFun a6989586621679253493 c6989586621679253492 -> Type) -> Type) (OnSym1 b6989586621679253491 a6989586621679253493 c6989586621679253492 l1) l2 = OnSym2 b6989586621679253491 a6989586621679253493 c6989586621679253492 l1 l2

data OnSym2 (l :: TyFun b6989586621679253491 (TyFun b6989586621679253491 c6989586621679253492 -> Type) -> Type) (l :: TyFun a6989586621679253493 b6989586621679253491 -> Type) (l :: TyFun a6989586621679253493 (TyFun a6989586621679253493 c6989586621679253492 -> Type)) #

Instances

SuppressUnusedWarnings ((TyFun b6989586621679253491 (TyFun b6989586621679253491 c6989586621679253492 -> Type) -> Type) -> (TyFun a6989586621679253493 b6989586621679253491 -> Type) -> TyFun a6989586621679253493 (TyFun a6989586621679253493 c6989586621679253492 -> Type) -> *) (OnSym2 b6989586621679253491 a6989586621679253493 c6989586621679253492) # 

Methods

suppressUnusedWarnings :: Proxy (OnSym2 b6989586621679253491 a6989586621679253493 c6989586621679253492) t -> () #

type Apply a6989586621679253493 (TyFun a6989586621679253493 c6989586621679253492 -> Type) (OnSym2 b6989586621679253491 a6989586621679253493 c6989586621679253492 l1 l2) l3 # 
type Apply a6989586621679253493 (TyFun a6989586621679253493 c6989586621679253492 -> Type) (OnSym2 b6989586621679253491 a6989586621679253493 c6989586621679253492 l1 l2) l3 = OnSym3 b6989586621679253491 a6989586621679253493 c6989586621679253492 l1 l2 l3

data OnSym3 (l :: TyFun b6989586621679253491 (TyFun b6989586621679253491 c6989586621679253492 -> Type) -> Type) (l :: TyFun a6989586621679253493 b6989586621679253491 -> Type) (l :: a6989586621679253493) (l :: TyFun a6989586621679253493 c6989586621679253492) #

Instances

SuppressUnusedWarnings ((TyFun b6989586621679253491 (TyFun b6989586621679253491 c6989586621679253492 -> Type) -> Type) -> (TyFun a6989586621679253493 b6989586621679253491 -> Type) -> a6989586621679253493 -> TyFun a6989586621679253493 c6989586621679253492 -> *) (OnSym3 b6989586621679253491 a6989586621679253493 c6989586621679253492) # 

Methods

suppressUnusedWarnings :: Proxy (OnSym3 b6989586621679253491 a6989586621679253493 c6989586621679253492) t -> () #

type Apply a c (OnSym3 b a c l1 l2 l3) l4 # 
type Apply a c (OnSym3 b a c l1 l2 l3) l4 = On b a c l1 l2 l3 l4

type OnSym4 (t :: TyFun b6989586621679253491 (TyFun b6989586621679253491 c6989586621679253492 -> Type) -> Type) (t :: TyFun a6989586621679253493 b6989586621679253491 -> Type) (t :: a6989586621679253493) (t :: a6989586621679253493) = On t t t t #