Generic.Data.Internal.Defun

Defunctionalization

See https://hackage.haskell.org/package/singletons-2.4.1/docs/src/Data-Singletons-Internal.html#TyFun

A copy of the defunctionalization implementation in the singletons package, to not pull in too heavy dependencies.

Documentation

data TyFun :: Type -> Type -> Type

type (~>) a b = TyFun a b -> Type infixr 0

Kind of function symbols

type family (f :: TyFun k1 k2 -> Type) @@ (x :: k1) :: k2 infixl 9

Instances

type (@@) k2 k2 (Id k2 k2) x

type (@@) k2 k2 (Id k2 k2) x = x

type (@@) k1 k2 (TyCon k1 k2 f) x

type (@@) k1 k2 (TyCon k1 k2 f) x = f x

type (@@) k1 k2 (Const k1 k2 t) x

type (@@) k1 k2 (Const k1 k2 t) x = t

data TyCon :: (k1 -> k2) -> TyFun k1 k2 -> Type

Type constructor function symbol

Instances

type (@@) k1 k2 (TyCon k1 k2 f) x

type (@@) k1 k2 (TyCon k1 k2 f) x = f x

data Id :: TyFun k1 k2 -> Type

Identity function symbol

Instances

type (@@) k2 k2 (Id k2 k2) x

type (@@) k2 k2 (Id k2 k2) x = x

data Const :: k2 -> TyFun k1 k2 -> Type

Constant function symbol

Instances

type (@@) k1 k2 (Const k1 k2 t) x

type (@@) k1 k2 (Const k1 k2 t) x = t