Hask 范畴上的函子
作者：互联网
Hask 范畴上的函子
Functor 对应的是 Haskell 中的 typeclass (类型类)
例
class Functor (f :: * -> *) where
fmap :: (a -> b) -> f a -> f b
这是 Haskell 中 Functor 的定义，Functor 映射态射的函数 fmap 没有定义。
用户自己给出 Functor instance 的 fmap 定义有没有可能不满足 Functor 两个公理？
第一个是有可能的
验证两个公理
1. \(F(id_A) = id_{F(A)}\)
反例
data T a = A | B deriving (Show, Eq)
instance Functor T where
fmap f A = A
fmap f B = A
-- fmap f = \_ -> A
g = fmap id A
g' = fmap id B
g'' = B == g'
此处 g'' 将返回 False，fmap id B = A，也就是说 fmap id != id
此处 HLS 仍有 lhint 提示:
Functor law
Found:
fmap id
Why not:
id
上例中
-
T:: 假设是 functor -
a,T a,f a,T (f a):: object. 此处T将所有 object 映射到同一 object，方便起见记为T _ -
a,f a在 Hask 的一个 subcategory，T a和T (f a)在另一个 subcategory -
A,B::T _这一 object 的 element -
T f::T _这一 object 上的 endomorphism
2. \(F(f\circ g) = F(f) \circ F(g)\)
不知道，群友说由 parametricity 保证
包括 f :: a -> a 推得 f = id 这种东西，我觉得是对的，但我不知道怎么证明。可能需要更多知识，但我连有几种多态都没记住，哈哈
标签：fmap,subcategory,函子,Hask,object,Functor,id,范畴 来源： https://www.cnblogs.com/human-in-human/p/16366522.html