Functor 对应的是 Haskell 中的 typeclass
(类型类)
class Functor (f :: * -> *) where fmap :: (a -> b) -> f a -> f b
这是 Haskell 中 Functor 的定义,Functor 映射态射的函数 fmap
没有定义。
用户自己给出 Functor instance 的 fmap
定义有没有可能不满足 Functor 两个公理?
第一个是有可能的
验证两个公理
反例
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
不知道,群友说由 parametricity 保证
包括 f :: a -> a
推得 f = id
这种东西,我觉得是对的,但我不知道怎么证明。可能需要更多知识,但我连有几种多态都没记住,哈哈