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_6989586621679292632 = 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_6989586621679292595 = Apply (Apply (Apply (Apply Lambda_6989586621679292600Sym0 f) g) a_6989586621679292595) a_6989586621679292595 

(%:.) :: 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_6989586621679304622 a_6989586621679304624 = Apply (Apply (Apply (Apply (Apply (Apply Lambda_6989586621679304630Sym0 ty) f) a_6989586621679304622) a_6989586621679304624) a_6989586621679304622) a_6989586621679304624 

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

Instances

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

Methods

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

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

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

data ConstSym0 (l :: TyFun a6989586621679292511 (TyFun b6989586621679292512 a6989586621679292511 -> Type)) #

Instances

SuppressUnusedWarnings (TyFun a6989586621679292511 (TyFun b6989586621679292512 a6989586621679292511 -> Type) -> *) (ConstSym0 b6989586621679292512 a6989586621679292511) # 

Methods

suppressUnusedWarnings :: Proxy (ConstSym0 b6989586621679292512 a6989586621679292511) t -> () #

type Apply a6989586621679292511 (TyFun b6989586621679292512 a6989586621679292511 -> Type) (ConstSym0 b6989586621679292512 a6989586621679292511) l # 
type Apply a6989586621679292511 (TyFun b6989586621679292512 a6989586621679292511 -> Type) (ConstSym0 b6989586621679292512 a6989586621679292511) l = ConstSym1 b6989586621679292512 a6989586621679292511 l

data ConstSym1 (l :: a6989586621679292511) (l :: TyFun b6989586621679292512 a6989586621679292511) #

Instances

SuppressUnusedWarnings (a6989586621679292511 -> TyFun b6989586621679292512 a6989586621679292511 -> *) (ConstSym1 b6989586621679292512 a6989586621679292511) # 

Methods

suppressUnusedWarnings :: Proxy (ConstSym1 b6989586621679292512 a6989586621679292511) 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 :: a6989586621679292511) (t :: b6989586621679292512) = Const t t #

data (:.$) (l :: TyFun (TyFun b6989586621679292508 c6989586621679292509 -> Type) (TyFun (TyFun a6989586621679292510 b6989586621679292508 -> Type) (TyFun a6989586621679292510 c6989586621679292509 -> Type) -> Type)) #

Instances

SuppressUnusedWarnings (TyFun (TyFun b6989586621679292508 c6989586621679292509 -> Type) (TyFun (TyFun a6989586621679292510 b6989586621679292508 -> Type) (TyFun a6989586621679292510 c6989586621679292509 -> Type) -> Type) -> *) ((:.$) b6989586621679292508 a6989586621679292510 c6989586621679292509) # 

Methods

suppressUnusedWarnings :: Proxy ((b6989586621679292508 :.$ a6989586621679292510) c6989586621679292509) t -> () #

type Apply (TyFun b6989586621679292508 c6989586621679292509 -> Type) (TyFun (TyFun a6989586621679292510 b6989586621679292508 -> Type) (TyFun a6989586621679292510 c6989586621679292509 -> Type) -> Type) ((:.$) b6989586621679292508 a6989586621679292510 c6989586621679292509) l # 
type Apply (TyFun b6989586621679292508 c6989586621679292509 -> Type) (TyFun (TyFun a6989586621679292510 b6989586621679292508 -> Type) (TyFun a6989586621679292510 c6989586621679292509 -> Type) -> Type) ((:.$) b6989586621679292508 a6989586621679292510 c6989586621679292509) l = (:.$$) b6989586621679292508 a6989586621679292510 c6989586621679292509 l

data (l :: TyFun b6989586621679292508 c6989586621679292509 -> Type) :.$$ (l :: TyFun (TyFun a6989586621679292510 b6989586621679292508 -> Type) (TyFun a6989586621679292510 c6989586621679292509 -> Type)) #

Instances

SuppressUnusedWarnings ((TyFun b6989586621679292508 c6989586621679292509 -> Type) -> TyFun (TyFun a6989586621679292510 b6989586621679292508 -> Type) (TyFun a6989586621679292510 c6989586621679292509 -> Type) -> *) ((:.$$) b6989586621679292508 a6989586621679292510 c6989586621679292509) # 

Methods

suppressUnusedWarnings :: Proxy ((b6989586621679292508 :.$$ a6989586621679292510) c6989586621679292509) t -> () #

type Apply (TyFun a6989586621679292510 b6989586621679292508 -> Type) (TyFun a6989586621679292510 c6989586621679292509 -> Type) ((:.$$) b6989586621679292508 a6989586621679292510 c6989586621679292509 l1) l2 # 
type Apply (TyFun a6989586621679292510 b6989586621679292508 -> Type) (TyFun a6989586621679292510 c6989586621679292509 -> Type) ((:.$$) b6989586621679292508 a6989586621679292510 c6989586621679292509 l1) l2 = (:.$$$) b6989586621679292508 a6989586621679292510 c6989586621679292509 l1 l2

data ((l :: TyFun b6989586621679292508 c6989586621679292509 -> Type) :.$$$ (l :: TyFun a6989586621679292510 b6989586621679292508 -> Type)) (l :: TyFun a6989586621679292510 c6989586621679292509) #

Instances

SuppressUnusedWarnings ((TyFun b6989586621679292508 c6989586621679292509 -> Type) -> (TyFun a6989586621679292510 b6989586621679292508 -> Type) -> TyFun a6989586621679292510 c6989586621679292509 -> *) ((:.$$$) b6989586621679292508 a6989586621679292510 c6989586621679292509) # 

Methods

suppressUnusedWarnings :: Proxy ((b6989586621679292508 :.$$$ a6989586621679292510) c6989586621679292509) 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 b6989586621679292508 c6989586621679292509 -> Type) (t :: TyFun a6989586621679292510 b6989586621679292508 -> Type) (t :: a6989586621679292510) = (:.) t t t #

data FlipSym0 (l :: TyFun (TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) (TyFun b6989586621679292506 (TyFun a6989586621679292505 c6989586621679292507 -> Type) -> Type)) #

Instances

SuppressUnusedWarnings (TyFun (TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) (TyFun b6989586621679292506 (TyFun a6989586621679292505 c6989586621679292507 -> Type) -> Type) -> *) (FlipSym0 b6989586621679292506 a6989586621679292505 c6989586621679292507) # 

Methods

suppressUnusedWarnings :: Proxy (FlipSym0 b6989586621679292506 a6989586621679292505 c6989586621679292507) t -> () #

type Apply (TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) (TyFun b6989586621679292506 (TyFun a6989586621679292505 c6989586621679292507 -> Type) -> Type) (FlipSym0 b6989586621679292506 a6989586621679292505 c6989586621679292507) l # 
type Apply (TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) (TyFun b6989586621679292506 (TyFun a6989586621679292505 c6989586621679292507 -> Type) -> Type) (FlipSym0 b6989586621679292506 a6989586621679292505 c6989586621679292507) l = FlipSym1 b6989586621679292506 a6989586621679292505 c6989586621679292507 l

data FlipSym1 (l :: TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) (l :: TyFun b6989586621679292506 (TyFun a6989586621679292505 c6989586621679292507 -> Type)) #

Instances

SuppressUnusedWarnings ((TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) -> TyFun b6989586621679292506 (TyFun a6989586621679292505 c6989586621679292507 -> Type) -> *) (FlipSym1 b6989586621679292506 a6989586621679292505 c6989586621679292507) # 

Methods

suppressUnusedWarnings :: Proxy (FlipSym1 b6989586621679292506 a6989586621679292505 c6989586621679292507) t -> () #

type Apply b6989586621679292506 (TyFun a6989586621679292505 c6989586621679292507 -> Type) (FlipSym1 b6989586621679292506 a6989586621679292505 c6989586621679292507 l1) l2 # 
type Apply b6989586621679292506 (TyFun a6989586621679292505 c6989586621679292507 -> Type) (FlipSym1 b6989586621679292506 a6989586621679292505 c6989586621679292507 l1) l2 = FlipSym2 b6989586621679292506 a6989586621679292505 c6989586621679292507 l1 l2

data FlipSym2 (l :: TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) (l :: b6989586621679292506) (l :: TyFun a6989586621679292505 c6989586621679292507) #

Instances

SuppressUnusedWarnings ((TyFun a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) -> b6989586621679292506 -> TyFun a6989586621679292505 c6989586621679292507 -> *) (FlipSym2 b6989586621679292506 a6989586621679292505 c6989586621679292507) # 

Methods

suppressUnusedWarnings :: Proxy (FlipSym2 b6989586621679292506 a6989586621679292505 c6989586621679292507) 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 a6989586621679292505 (TyFun b6989586621679292506 c6989586621679292507 -> Type) -> Type) (t :: b6989586621679292506) (t :: a6989586621679292505) = 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 a6989586621679304576 (TyFun (TyFun a6989586621679304576 b6989586621679304577 -> Type) b6989586621679304577 -> Type)) #

Instances

SuppressUnusedWarnings (TyFun a6989586621679304576 (TyFun (TyFun a6989586621679304576 b6989586621679304577 -> Type) b6989586621679304577 -> Type) -> *) ((:&$) a6989586621679304576 b6989586621679304577) # 

Methods

suppressUnusedWarnings :: Proxy (a6989586621679304576 :&$ b6989586621679304577) t -> () #

type Apply a6989586621679304576 (TyFun (TyFun a6989586621679304576 b6989586621679304577 -> Type) b6989586621679304577 -> Type) ((:&$) a6989586621679304576 b6989586621679304577) l # 
type Apply a6989586621679304576 (TyFun (TyFun a6989586621679304576 b6989586621679304577 -> Type) b6989586621679304577 -> Type) ((:&$) a6989586621679304576 b6989586621679304577) l = (:&$$) a6989586621679304576 b6989586621679304577 l

data (l :: a6989586621679304576) :&$$ (l :: TyFun (TyFun a6989586621679304576 b6989586621679304577 -> Type) b6989586621679304577) #

Instances

SuppressUnusedWarnings (a6989586621679304576 -> TyFun (TyFun a6989586621679304576 b6989586621679304577 -> Type) b6989586621679304577 -> *) ((:&$$) a6989586621679304576 b6989586621679304577) # 

Methods

suppressUnusedWarnings :: Proxy (a6989586621679304576 :&$$ b6989586621679304577) 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 :: a6989586621679304576) (t :: TyFun a6989586621679304576 b6989586621679304577 -> Type) = (:&) t t #

data OnSym0 (l :: TyFun (TyFun b6989586621679304578 (TyFun b6989586621679304578 c6989586621679304579 -> Type) -> Type) (TyFun (TyFun a6989586621679304580 b6989586621679304578 -> Type) (TyFun a6989586621679304580 (TyFun a6989586621679304580 c6989586621679304579 -> Type) -> Type) -> Type)) #

Instances

SuppressUnusedWarnings (TyFun (TyFun b6989586621679304578 (TyFun b6989586621679304578 c6989586621679304579 -> Type) -> Type) (TyFun (TyFun a6989586621679304580 b6989586621679304578 -> Type) (TyFun a6989586621679304580 (TyFun a6989586621679304580 c6989586621679304579 -> Type) -> Type) -> Type) -> *) (OnSym0 b6989586621679304578 a6989586621679304580 c6989586621679304579) # 

Methods

suppressUnusedWarnings :: Proxy (OnSym0 b6989586621679304578 a6989586621679304580 c6989586621679304579) t -> () #

type Apply (TyFun b6989586621679304578 (TyFun b6989586621679304578 c6989586621679304579 -> Type) -> Type) (TyFun (TyFun a6989586621679304580 b6989586621679304578 -> Type) (TyFun a6989586621679304580 (TyFun a6989586621679304580 c6989586621679304579 -> Type) -> Type) -> Type) (OnSym0 b6989586621679304578 a6989586621679304580 c6989586621679304579) l # 
type Apply (TyFun b6989586621679304578 (TyFun b6989586621679304578 c6989586621679304579 -> Type) -> Type) (TyFun (TyFun a6989586621679304580 b6989586621679304578 -> Type) (TyFun a6989586621679304580 (TyFun a6989586621679304580 c6989586621679304579 -> Type) -> Type) -> Type) (OnSym0 b6989586621679304578 a6989586621679304580 c6989586621679304579) l = OnSym1 b6989586621679304578 a6989586621679304580 c6989586621679304579 l

data OnSym1 (l :: TyFun b6989586621679304578 (TyFun b6989586621679304578 c6989586621679304579 -> Type) -> Type) (l :: TyFun (TyFun a6989586621679304580 b6989586621679304578 -> Type) (TyFun a6989586621679304580 (TyFun a6989586621679304580 c6989586621679304579 -> Type) -> Type)) #

Instances

SuppressUnusedWarnings ((TyFun b6989586621679304578 (TyFun b6989586621679304578 c6989586621679304579 -> Type) -> Type) -> TyFun (TyFun a6989586621679304580 b6989586621679304578 -> Type) (TyFun a6989586621679304580 (TyFun a6989586621679304580 c6989586621679304579 -> Type) -> Type) -> *) (OnSym1 b6989586621679304578 a6989586621679304580 c6989586621679304579) # 

Methods

suppressUnusedWarnings :: Proxy (OnSym1 b6989586621679304578 a6989586621679304580 c6989586621679304579) t -> () #

type Apply (TyFun a6989586621679304580 b6989586621679304578 -> Type) (TyFun a6989586621679304580 (TyFun a6989586621679304580 c6989586621679304579 -> Type) -> Type) (OnSym1 b6989586621679304578 a6989586621679304580 c6989586621679304579 l1) l2 # 
type Apply (TyFun a6989586621679304580 b6989586621679304578 -> Type) (TyFun a6989586621679304580 (TyFun a6989586621679304580 c6989586621679304579 -> Type) -> Type) (OnSym1 b6989586621679304578 a6989586621679304580 c6989586621679304579 l1) l2 = OnSym2 b6989586621679304578 a6989586621679304580 c6989586621679304579 l1 l2

data OnSym2 (l :: TyFun b6989586621679304578 (TyFun b6989586621679304578 c6989586621679304579 -> Type) -> Type) (l :: TyFun a6989586621679304580 b6989586621679304578 -> Type) (l :: TyFun a6989586621679304580 (TyFun a6989586621679304580 c6989586621679304579 -> Type)) #

Instances

SuppressUnusedWarnings ((TyFun b6989586621679304578 (TyFun b6989586621679304578 c6989586621679304579 -> Type) -> Type) -> (TyFun a6989586621679304580 b6989586621679304578 -> Type) -> TyFun a6989586621679304580 (TyFun a6989586621679304580 c6989586621679304579 -> Type) -> *) (OnSym2 b6989586621679304578 a6989586621679304580 c6989586621679304579) # 

Methods

suppressUnusedWarnings :: Proxy (OnSym2 b6989586621679304578 a6989586621679304580 c6989586621679304579) t -> () #

type Apply a6989586621679304580 (TyFun a6989586621679304580 c6989586621679304579 -> Type) (OnSym2 b6989586621679304578 a6989586621679304580 c6989586621679304579 l1 l2) l3 # 
type Apply a6989586621679304580 (TyFun a6989586621679304580 c6989586621679304579 -> Type) (OnSym2 b6989586621679304578 a6989586621679304580 c6989586621679304579 l1 l2) l3 = OnSym3 b6989586621679304578 a6989586621679304580 c6989586621679304579 l1 l2 l3

data OnSym3 (l :: TyFun b6989586621679304578 (TyFun b6989586621679304578 c6989586621679304579 -> Type) -> Type) (l :: TyFun a6989586621679304580 b6989586621679304578 -> Type) (l :: a6989586621679304580) (l :: TyFun a6989586621679304580 c6989586621679304579) #

Instances

SuppressUnusedWarnings ((TyFun b6989586621679304578 (TyFun b6989586621679304578 c6989586621679304579 -> Type) -> Type) -> (TyFun a6989586621679304580 b6989586621679304578 -> Type) -> a6989586621679304580 -> TyFun a6989586621679304580 c6989586621679304579 -> *) (OnSym3 b6989586621679304578 a6989586621679304580 c6989586621679304579) # 

Methods

suppressUnusedWarnings :: Proxy (OnSym3 b6989586621679304578 a6989586621679304580 c6989586621679304579) 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 b6989586621679304578 (TyFun b6989586621679304578 c6989586621679304579 -> Type) -> Type) (t :: TyFun a6989586621679304580 b6989586621679304578 -> Type) (t :: a6989586621679304580) (t :: a6989586621679304580) = On t t t t #