函數法是否證明結構的完整保存？

在Data.Functor的文檔中，以下兩個作爲仿函數法則，所有仿函數都應遵守。函數法是否證明結構的完整保存？

fmap id == id 
fmap (f . g) == fmap f . fmap g

我直覺告訴我函數子應該工作的方式是，他們應該是「結構保存」，或者換句話說，如果你有一個函數f :: a -> b和它的逆g :: b -> a然後

fmap f . fmap g == id

我一直沒有能夠拿出執行fmap這將堅持前兩個法律和違反第二，但這是很難證明。有人能夠啓發我嗎？

來源

2014-05-15 kqr

+1我一直在努力解決類似的問題。有這樣一個直覺的表述困擾着我的一件事情：沒有反向的函數呢？當然'fmap（const「Foo」）在某種意義上也是結構保存的？ – duplode

是的，但你不能用'const「Foo」'來證明法則是正確的 - 你必須選擇另一個函數。我並不是說仿函子只適用於法律涵蓋的各種功能。 – kqr

@duplode想象一棵樹'data Tree a = Leaf |節點a [樹a]'。當我們談論「t :: Tree a」的「結構」時，我們考慮每個節點有多少個子樹，以及這些子樹如何排列。所以你可能會說我們對't'感興趣，它的節點中有_什麼。實際上我們可以用'fmap（const（））t'來捕獲它。 – fizruk

其實，你的「第三」仿函數法從實際仿法律直接跟隨而事實上，f . g ≡ id：

fmap f . fmap g ≡ fmap (f . g) ≡ fmap id ≡ id

還有更多：哈斯克爾確保，如果第一定律適用於Functor實例，那麼第二個也是成立的（這是一個fmap類型的自由定理）。即您必須爲您的Functor實例證明只有fmap id ≡ id法律才能確保其有效。

來源

2014-05-15 10:24:39 fizruk

當'f。 g≡id'，函數f'和'g'是否有描述它們之間關係的數學術語？（我認爲我在某處讀同構，但我不確定） – Sibi

@Sibi：爲什麼，'f'是'g'的左倒數，'g'是'f'的右倒數。這並不意味着任何一個函數的domain和codomain同構，儘管'show :: Int - > String'具有'read'作爲左反函數，但'Int'明顯具有小於'String'的基數。 – leftaroundabout

@Sibi請注意'f。 g≡id'並不意味着'g。 f≡id'。但是，如果是這種情況，那麼這兩個函數都稱爲_「同構」_。否則，'f'被稱爲_「撤回」_（或_「'g'」_）的左反，而'g'被稱爲_「部分」_（或_「與」f「的右倒數」_）。 – fizruk

函數法是否證明結構的完整保存？

回答

相關問題