Is it possible to construct a kind level identity which maps a kind a
to the same kind a
in haskell ?
Here are some non-answers :
type One :: * -> *
newtype One a = One {unOne :: a}
-- >>> :kind! 'One
-- 'One :: a -> One a -- not the identity
-- = 'One
type family Id a where -- *pointwise* identity, not a function (can't not apply it)
Id a = a
CodePudding user response:
Currently the type language is first-order, meaning unmatchable functions like Id
must be fully saturated: Higher-Order Type-Level Programming in Haskell.
A proposal has been accepted to remedy this: Unsaturated type families.
Under this proposal we distinguish between the kind of One :: Type -> Type
and Id :: k -> k
; One
is matchable and Id
is unmatchable:
One :: Type -> @M Type
Id :: k -> @U k
and we will be able to pass unmatchable type-level functions as arguments:
data Foo :: (Type -> @U Type) -> Type
data Foo f = MkFoo (f Int) (f Bool) (f Char)
foo :: Foo Id
foo = MkFoo 10 False 'a'
This will allow you to construct proper identity functors, functor composition and categorical gadgets.
type Functor :: (s -> @m t) -> Constraint
class (Category (Source f), Category (Target f))
=> Functor (f :: s -> @m t) where
type Source (f :: s -> @m t) :: Cat s
type Target (f :: s -> @m t) :: Cat t
fmap :: Source f a a' -> Target f (f a) (f a')
type IdFunctor :: Cat ob -> ob -> ob
type IdFunctor cat a = a
instance Category @ob cat => Functor (IdFunctor @ob cat) where
type Source (IdFunctor cat) = cat
type Target (IdFunctor cat) = cat
fmap :: cat a a' -> cat a a'
fmap = id