kind level identity in haskell

user_242189 0
Viewed 86

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
type-families haskell
1 Answers

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
user_1658060
Related