是否有可能在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
最佳答案
目前的类型语言是一阶，这意味着像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
关于haskell - Haskell中的种类级别身份，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/71277039/