haskell - Haskell中的种类级别身份

Question

是否有可能在haskell中构造一个将一种类型a映射到同一种类型a的类型级别标识？

以下是一些非答案:

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

Answer 1

目前的类型语言是一阶，这意味着像Id这样无法匹配的函数必须是完全饱和的:Higher-Order Type-Level Programming in Haskell .

已接受解决此问题的建议:Unsaturated type families .

在这个提议下，我们区分了 One::Type -> Type 和 Id::k -> k 的种类； One 可匹配，Id 不可匹配:

One :: Type -> @M Type
Id  :: k    -> @U k

我们将能够将无法匹配的类型级函数作为参数传递:

data Foo :: (Type -> @U Type) -> Type
data Foo f = MkFoo (f Int) (f Bool) (f Char)

foo :: Foo Id
foo = MkFoo 10 False 'a'

这将允许您构造适当的身份仿函数、仿函数组合和分类小工具。

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