Something of kind
a ~> b is a defunctionalized type
function that is not necessarily generative or injective.
Defunctionalized type functions (also called "defunctionalization
symbols") can be partially applied, even if the original type function
cannot be. For more information on how this works, see the "Promotion
and partial application" section of the
README.
The singleton for things of kind
a ~> b is
SLambda.
SLambda values can be constructed in one of two
ways:
- With the singFun* family of combinators (e.g.,
singFun1). For example, if you have:
type Id :: a -> a
sId :: Sing a -> Sing (Id a)
Then you can construct a value of type
Sing @(a
~> a) (that is,
SLambda @a @a like so:
sIdFun :: Sing @(a ~> a) IdSym0
sIdFun = singFun1 @IdSym0 sId
Where
IdSym0 :: a ~> a is the defunctionlized
version of
Id.
- Using the SingI class. For example, sing
@IdSym0 is another way of defining sIdFun above. The
singletons-th library automatically generates SingI
instances for defunctionalization symbols such as
IdSym0.
Normal type-level arrows
(->) can be converted into
defunctionalization arrows
(~>) by the use of the
TyCon family of types. (Refer to the Haddocks for
TyCon1
to see an example of this in practice.) For this reason, we do not
make an effort to define defunctionalization symbols for most type
constructors of kind
a -> b, as they can be used in
defunctionalized settings by simply applying
TyCon{N} with an
appropriate
N.
This includes the
(->) type constructor itself, which is
of kind
Type -> Type -> Type. One
can turn it into something of kind
Type ~>
Type ~> Type by writing
TyCon2
(->), or something of kind
Type -> Type
~> Type by writing
TyCon1 ((->)
t) (where
t :: Type).