Hask 范畴上的函子

2022/6/11 23:52:11

本文主要是介绍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'' 将返回 Falsefmap 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 aHask 的一个 subcategory,T aT (f a) 在另一个 subcategory

  • A, B :: T _ 这一 object 的 element

  • T f :: T _ 这一 object 上的 endomorphism

<iframe class="quiver-embed" height="432" src="https://q.uiver.app/?q=WzAsNixbMiwwLCJcXHRleHR7QX0iLFsyNDAsNjAsNjAsMV1dLFsyLDIsIlxcdGV4dHtBfSIsWzI0MCw2MCw2MCwxXV0sWzMsMCwiXFx0ZXh0e0J9IixbMjQwLDYwLDYwLDFdXSxbMywyLCJcXHRleHR7Qn0iLFsyNDAsNjAsNjAsMV1dLFswLDAsImEiLFswLDYwLDYwLDFdXSxbMCwyLCJcXHRleHR7ZiBhfSIsWzAsNjAsNjAsMV1dLFswLDEsIlxcdGV4dHtUIGZ9IiwwLHsiY29sb3VyIjpbMjQwLDYwLDYwXX0sWzI0MCw2MCw2MCwxXV0sWzIsMSwiIiwyLHsiY29sb3VyIjpbMjQwLDYwLDYwXX1dLFs0LDUsIlxcdGV4dHtmfSIsMix7ImNvbG91ciI6WzAsNjAsNjBdfSxbMCw2MCw2MCwxXV0sWzUsMSwiXFx0ZXh0e1R9Il0sWzQsMCwiXFx0ZXh0e1R9Il0sWzgsNiwiXFx0ZXh0e1R9IiwwLHsic2hvcnRlbiI6eyJzb3VyY2UiOjIwLCJ0YXJnZXQiOjIwfX1dXQ==&embed" style="border-radius: 8px; border: none" width="560"></iframe>

2. \(F(f\circ g) = F(f) \circ F(g)\)

不知道,群友说由 parametricity 保证

包括 f :: a -> a 推得 f = id 这种东西,我觉得是对的,但我不知道怎么证明。可能需要更多知识,但我连有几种多态都没记住,哈哈



这篇关于Hask 范畴上的函子的文章就介绍到这儿,希望我们推荐的文章对大家有所帮助,也希望大家多多支持为之网!


扫一扫关注最新编程教程