1樓：應用
寫一點個人感悟吧。由於是個人感悟注重思路，細節可能不夠全面可能有錯誤，希望大家指正。
就我看來，公尺田引理很晚才提出來－－這件事情本身就比較怪異。
函子hA= Hom(A, )被提出來的時候就暗含了公尺田引理。
首先不同函子之間滿足自然變換。
自然變化實質是說同乙個型別裡的同乙個元素被不同函子對映的不同型別的不同值時，對映值之間存在簡單的對應關係。
ＣＥＤ為範疇，FG為函子。
假設有範疇Ｍ
選取 a -> _ 的所有函式 ：
形成函子hａ= Hom(ａ, )如下：
Ｔa 表示型別a -> a ,Tb 表示型別a->b ,Tc 表示型別a -> c
現在的問題是Ｔa,Tb,Tc中的元素和ａ,b,c中的元素存在怎樣的對應關係？
公尺田引理告訴我們：只要你指定了Ta 中id (a -> a ) 元素對應ａ中的值，那麼Ｔa,Tb,Tc中的元素和ａ,b,c中的元素的對應關係都確定下來了。
在Ｍ中選擇ｆ :: (a->b)
f 在hａ中存在於兩個地方：Ta 中 Ta -> Tb (f 。)
idTava
f 。:: (Ta -> Tb) --- fa -> b
fTbf v :: b
id 對應值有多少選擇呢？有ａ中元素個數數量的選擇。
假設有乙個函子Ｆ將Ｍ函子變換為Ｎ函子：
idTava
f 。:: (Ta -> Tbfa -> Ｆb
fTbf Ｆv ::Ｆb
id 對應值有多少選擇呢？有Ｆａ中元素個數數量的選擇。每一種選擇都是一種自然變換。
所以：ｉｄ函式在這個過程中有巨大的作用，宛如一座燈塔。對於海上的船隻來說，燈塔的位置就代表了整個大陸的位置。選定了燈塔位置，整個大陸的位置也確定了。
反公尺田引理
同樣的推理：
至於Ｔａ 中ｉｄ的選擇範圍是Ｔ'ａ (Hom(A,B)) ,所以:
很好理解。
@parker liu 的例子：
imager
::forallr.
((Bool
->r)
->[r
])imager
iffie
=fmap
iffie
[True
,False
,True
,True
]data
Color
=Red
|Green
|Blue
deriving
Show
data
Note=C
|D|E
|F|G
|A|B
deriving
Show
colorMapx=
ifxthen
Blue
else
RedheatMapx=
ifxthen
32else
212soundMapx=
ifxthen
Celse
GidBool
::Bool
->Bool
idBoolx=
xmain=do
$imager
idBool
$imager
colorMap
$imager
soundMap
這句:imager :: forall r . ((Bool -> r) -> [r])
imager iffie = fmap iffie [True, False, True, True]
就是指定 id為 [True, False, True, True].
之後，任何Bool -> r 的函式都能等價到相應的[r].
2樓：
其他回答和鏈結對於問題來龍去脈都講的很清楚了。從我個人的直覺，只從怎麼用來說，就是CPS，可以用來改善一些程式的漸進時間複雜度。
3樓：parker liu
Yoneda lemma in nLab
好了，下面讓我們開始來了解公尺田引理吧。
公尺田引理的定義如下：
其意義是從函子h
A = Hom(A, )到函子F的自然變換和F(A)的元素一一對應。即任意給定乙個這樣的自然變換Φ，我們都可以找到乙個F(A)中的元素u，該元素u由這個自然變換唯一決定，如下所示：
反變模式的公尺田引理定義如下：
這裡的自然變換是反變函子h
A = Hom(, A)到函子G的自然變換。如果將函子G替換為反變函子hB = Hom(, B)，我們就得到了如下的同構形式
由此可以得到公尺田嵌入，即範疇C到範疇Cop →Set的函子，如下所示：
這裡h_是乙個fully faithful的函子，也就是一一對應的函子。
好了，現在讓我們回到Haskell的世界來看看Yoneda是什麼樣的。
按照上面的定義，我們可以在Haskell中定義如下的Yoneda和Coyoneda資料型別：
newtype
Yonedafa
=Yoneda
instance
Functor
(Yonedaf)
where
fmapfy
=Yoneda$\
k->runYoneday(
k.f)
data
Coyonedafa
=forallb.
Coyoneda(b
->a)
(fb)
instance
Functor
(Coyonedaf)
where
fmapf(
Coyonedagv
)=Coyoneda(f
.g)v
>:t
fmap
fmap
::Functor
f=>(a
->b)
->fa
->fb
Prelude
>:t
flip
fmap
flip
fmap
::Functor
f=>fa
->(a
->b)
->fb
Prelude
>:t
uncurry
fmap
uncurry
fmap
::Functor
f=>(a
->b,
fa)->fb
-- The Yoneda is natural isomorphism between (f a) and ((a -> b) -> f b),
-- it just is the fmap that hide the parameter f a.
Prelude
>letyoneda
=flip
fmap
Prelude
>:t
yoneda
yoneda
::Functor
f=>fa
->(a
->b)
->fb
-- The Coyoneda is natural isomorphism between (b -> a, f b) and (f a) ,
-- it just get from parameter of uncurried fmap.
Prelude
>letcoyoneda
=uncurry
fmap
Prelude
>:t
coyoneda
coyoneda
::Functor
f=>(a
->b,
fa)->fb
由上面的實際驗證可以看到，Yoneda就是隱藏了引數f a的fmap，而Coyoneda就是fmap反柯里化後的引數構成的。
我們如何找出Yoneda中隱藏的引數f a呢，很簡單，只需要給Yoneda傳遞乙個id函式即可，如下所示：
lowerYoneda
::Yonedafa
->fa
lowerYoneda
(Yonedayf)
=yfid來自Understanding Yoneda的實際應用例子如下
imager
::forallr.
((Bool
->r)
->[r
])imager
iffie
=fmap
iffie
[True
,False
,True
,True
]data
Color
=Red
|Green
|Blue
deriving
Show
data
Note=C
|D|E
|F|G
|A|B
deriving
Show
colorMapx=
ifxthen
Blue
else
RedheatMapx=
ifxthen
32else
212soundMapx=
ifxthen
Celse
GidBool
::Bool
->Bool
idBoolx=
xmain=do
$imager
idBool
$imager
colorMap
$imager
soundMap
而對Coyoneda，要得到對應的f a，則只要簡單的應用fmap到構成Coyoneda的引數即可，如下所示：
lowerCoyoneda
::Coyonedafa
->fa
lowerCoyoneda
(Coyonedagv
)=fmapgv
我覺得公尺田引理更重要的是誘導出了一對伴隨函子(adjoint functor) ，左伴隨函子(A ) 和右伴隨函子Hom(A, )，從而得到如下的恒等式：
Hom(A B, C) Hom(B, Hom(A, C))
更直觀些的形式如下所示：
Hom(CopC,Set)Hom(C,[Cop,Set])
上面的恒等式表明等式的左右兩邊之間存在乙個自然同構(natural isomorphism)。右邊代是公尺田嵌入，而左邊就是hom-functor --Hom(-, -)，即在Haskell中就是非常常見的(->)，這是乙個Profunctor。因此由公尺田嵌入得到了乙個很基礎的Profunctor (->)，(->)有兩個引數，左邊的第乙個引數是反變的，右邊的第二個引數是協變的，我們有如下的Profunctor和(->)的定義：
class
Profunctor
pwhere
dimap::(
a->b)
->(c
->d)
->pb
c->pa
ddimapgh
=lmapg.
rmap
hinstance
Profunctor
(->)where
-- dimap g h f = h . f . g
dimap=(
>*<)lmap
=flip(.
)rmap=(
.)infixr
4>*<
(>*<)::
(a->b)
->(c
->d)
->(b
->c)
->(a
->d)
f>* \h->g. h.f因為(->)是Profunctor，並根據公尺田引理我們可以得到如下的交換圖： 上面的交換圖也可以通過運算子(.)和函式f, h的組合得到，具體如下： Prelude >lethomAf(f ::(b->b1))=( f.)Prelude >lethomhB(h ::(a1->a)) =(.h )Prelude >lethomhBAf(h ::(a1->a)) (f::( b->b1)) =homhBh. homAf fPrelude >lethomAfhB(h ::(a1->a)) (f::( b->b1)) =homAff. homhB hPrelude >:t homhBAf homhBAf::( a1->a) ->(b ->b1) ->(a ->b) ->a1-> b1Prelude >:t homAfhB homAfhB::( a1->a) ->(b ->b1) ->(a ->b) ->a1-> b1adjoint functor in nLab Yoneda lemma in nLab 維基百科: Hom functor 其實中文可以廣泛應用在高階語言中的變數命名上。比如const水果 李子 香蕉 菠蘿 It works. 風吃風 我覺得無所謂，就算用英文，常用的非變數詞也就那麼幾個，包一層改成中文有啥不行。再說變數也有好多人寫拼音 如果這些語言結構都是國內開發的，或者有一天不需要顧慮國外應用方，或者不需要去網路查b... 喵觀委執委會 沒想到乙個學習程式設計的工程人員，還會糾結名實之爭 引用一句小六子的話 好用的話，抓來用就好。pascal 倒是蠻糾結，吃飽了撐的區分 prosedure 和function 然後呢？掛了吧 龍捲風 數學的函式，只有數字，而計算的物件，就非常多，硬體 顯示器 鍵盤 滑鼠等非常多東西，計... 從此以後 這幾年程式設計確實挺火的，很多孩子都在學，市面上也看到挺多品牌的，對於家長們來說，選擇確實有難度，畢竟大夥兒基本都不大了解程式設計。其實專業方面各個機構目前差異不大，都是用麻省理工Scratch那一套東西，好一些的機構就自己再改編一下，研發一下。我覺得既然是培訓，那本質就還是教育，和我們平...為什麼很多人反對中文在程式設計中的使用？
在程式設計時呼叫的function對應的語義偏向「功能」還是「函式」？
讓孩子在程式設計貓學習程式設計，是好的選擇嗎？