Data.Singletons

Main singleton definitions

data family Sing (a :: k)

class SingI a

class SingKind k

Working with singletons

type KindOf a

type Demote a

data SingInstance a

data SomeSing k

singInstance

withSingI

withSomeSing

singByProxy

singByProxy#

withSing

singThat

Defunctionalization

data TyFun

type a ~> b

data TyCon1

data TyCon2

data TyCon3

data TyCon4

data TyCon5

data TyCon6

data TyCon7

data TyCon8

type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

type a @@ b

Defunctionalized singletons

singFun1

singFun2

singFun3

singFun4

singFun5

singFun6

singFun7

singFun8

unSingFun1

unSingFun2

unSingFun3

unSingFun4

unSingFun5

unSingFun6

unSingFun7

unSingFun8

type SingFunction1 f

type SingFunction2 f

type SingFunction3 f

type SingFunction4 f

type SingFunction5 f

type SingFunction6 f

type SingFunction7 f

type SingFunction8 f

Auxiliary functions

data Proxy k t