标签:fmap subcategory 函子 Hask object Functor id 范畴
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
<iframe class="quiver-embed" height="432" src="https://q.uiver.app/?q=WzAsNCxbMCwwLCJcXHRleHR7YX0iLFswLDYwLDYwLDFdXSxbMiwwLCJcXHRleHR7VCBhfSIsWzI0MCw2MCw2MCwxXV0sWzAsMiwiXFx0ZXh0e2YgYX0iLFswLDYwLDYwLDFdXSxbMiwyLCJcXHRleHR7VCAoZiBhKX0iLFsyNDAsNjAsNjAsMV1dLFsyLDMsIlxcdGV4dHtUfSJdLFswLDIsIlxcdGV4dHtmfSIsMix7ImNvbG91ciI6WzAsNjAsNjBdfSxbMCw2MCw2MCwxXV0sWzEsMywiXFx0ZXh0e1QgZiA9IGZtYXAgZn0iLDEseyJjb2xvdXIiOlsyNDAsNjAsNjBdfSxbMjQwLDYwLDYwLDFdXSxbMCwxLCJcXHRleHR7VH0iXSxbNSw2LCJcXHRleHR7VCA9IGZtYXB9IiwwLHsic2hvcnRlbiI6eyJzb3VyY2UiOjIwLCJ0YXJnZXQiOjMwfX1dXQ==&embed" style="border-radius: 8px; border: none" width="456"></iframe>
上例中
-
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
本站声明: 1. iCode9 技术分享网(下文简称本站)提供的所有内容,仅供技术学习、探讨和分享; 2. 关于本站的所有留言、评论、转载及引用,纯属内容发起人的个人观点,与本站观点和立场无关; 3. 关于本站的所有言论和文字,纯属内容发起人的个人观点,与本站观点和立场无关; 4. 本站文章均是网友提供,不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属;如您发现该文章侵犯了您的权益,可联系我们第一时间进行删除; 5. 本站为非盈利性的个人网站,所有内容不会用来进行牟利,也不会利用任何形式的广告来间接获益,纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。