ICode9

精准搜索请尝试: 精确搜索
首页 > 其他分享> 文章详细

Hask 范畴上的函子

2022-06-11 19:03:21  阅读:129  来源: 互联网

标签: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'' 将返回 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 这种东西,我觉得是对的,但我不知道怎么证明。可能需要更多知识,但我连有几种多态都没记住,哈哈

标签:fmap,subcategory,函子,Hask,object,Functor,id,范畴
来源: https://www.cnblogs.com/human-in-human/p/16366522.html

本站声明: 1. iCode9 技术分享网(下文简称本站)提供的所有内容,仅供技术学习、探讨和分享;
2. 关于本站的所有留言、评论、转载及引用,纯属内容发起人的个人观点,与本站观点和立场无关;
3. 关于本站的所有言论和文字,纯属内容发起人的个人观点,与本站观点和立场无关;
4. 本站文章均是网友提供,不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属;如您发现该文章侵犯了您的权益,可联系我们第一时间进行删除;
5. 本站为非盈利性的个人网站,所有内容不会用来进行牟利,也不会利用任何形式的广告来间接获益,纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。

专注分享技术,共同学习,共同进步。侵权联系[81616952@qq.com]

Copyright (C)ICode9.com, All Rights Reserved.

ICode9版权所有