函子自由單子和固定點之間的區別？

我正在閱讀http://www.haskellforall.com/2013/06/from-zero-to-cooperative-threads-in-33.html，其中抽象語法樹被派生爲代表一組指令的函子的自由單子。我注意到免費monad Free與函子Fix上的fixpoint運算符沒有什麼不同。函子自由單子和固定點之間的區別？

本文使用monad操作和do語法以簡明的方式構建這些AST（固定點）。我想知道這是否是免費monad實例的唯一好處？還有其他有趣的應用程序嗎？

來源

2013-06-25 Daniel Velkov

單子實例的主要好處是'do'符號和從'Control.Monad'組合子（如'replicateM_'和'forM_'在實施例中）的重複使用。一個常見的技巧是使用免費的monad構建類型，但要求結果的類型爲FreeT f m Void，以便它可以轉換爲函子的固定點。 –

'Monad'實例豐富了'Fix'的兩件事情 - 從'return'確定終止，從'（>> =）'自然擴展「。一個普通的'（Fix f）'不能保證有任何（有限的）值（即'（Fix Identity）'），但是'（Free f）'總是至少被'Pure'所居住。 –

@GabrielGonzalez你能否詳細說明你評論的第二部分？什麼是一個示例用例？ –

（NB這個組合從兩個礦和@以上Gabriel的評論了一下。）

這有可能爲Functor的Fix ED點的每一個居民是無限的，即let x = (Fix (Id x)) in x === (Fix (Id (Fix (Id ...))))是的唯一居民Fix Identity。 Free與Fix立即不同，因爲它確保至少有一個有限的Free f居民。事實上，如果Fix f有任何無限的居民，那麼Free f就有無限多的有限居民。

此無界限的另一個直接副作用是Functor f => Fix f不再是Functor。我們需要執行fmap :: Functor f => (a -> b) -> (f a -> f b)，但是Fix已經填充了f a中的「填滿所有洞」，因此我們不再有任何a將我們的fmap'd函數應用於。

這是創建Monad重要，因爲我們想實現return :: a -> Free f a和有，比方說，這項法律持fmap f . return = return . f，但它甚至沒有任何意義的Functor f => Fix f。

那麼如何Free「修復」這些Fix點缺陷？它用Pure構造函數「擴充」我們的基函數。因此，對於所有的Functor f,Pure :: a -> Free f a。這是我們保證有限的這種類型的居民。它也立刻給了我們一個好的定義return。

return = Pure

所以，你可能會認爲這除了由Fix取出可能是無限的「樹」創建嵌套Functor S和一些數量的「活」芽，由Pure代表的混合。我們使用return創建新芽，這可能被解釋爲承諾稍後「返回」該芽，並添加更多計算。實際上，這正是flip (>>=) :: (a -> Free f b) -> (Free f a -> Free f b)所做的。鑑於可應用於類型a的「繼續」功能f :: a -> Free f b，我們將樹返回到每個Pure a，並將其替換爲計算爲f a的延續。這讓我們「成長」我們的樹。

現在，Free顯然比Fix比較一般。爲了驅動這個家，有可能看到Functor f => Fix f作爲相應的Free f a的子類型！只需選擇a ~ Void我們有data Void = Void Void（即，一個不能構造的類型，是空的類型，沒有實例）。

爲了使它更清楚，我們可以用break :: Fix f -> Free f a打破我們Fix倒是Functor秒，然後嘗試用affix :: Free f Void -> Fix f顛倒了。

break (Fix f) = Free (fmap break f) 
affix (Free f) = Fix (fmap affix f)

首先注意到affix並不需要處理Pure x情況，因爲在這種情況下x :: Void，因而不能真正在那裏，所以Pure x是荒謬的，我們就忽略它。

還要注意的是break的返回類型是有點微妙，因爲a型只出現在返回類型，Free f a，使得它完全無法訪問的break任何用戶。「完全無法訪問」和「無法實例化」給了我們第一個暗示，儘管類型是affix和break是反向的，但我們可以證明它。

(break . affix) (Free f) 
===          [definition of affix] 
break (Fix (fmap affix f)) 
===          [definition of break] 
Free (fmap break (fmap affix f)) 
===          [definition of (.)] 
Free ((fmap break . fmap affix) f) 
===          [functor coherence laws] 
Free (fmap (break . affix) f)

哪些應該顯示（共感應，或者只是直觀，也許），該(break . affix)是一個身份。另一個方向以完全相同的方式進行。

因此，希望這表明Free f大於Fix f對於所有Functor f。

那麼爲什麼要用Fix？那麼，有時你只需要Free f Void的屬性，這是由於分層f的某些副作用。在這種情況下，調用它Fix f可以更清楚地表明，我們不應該嘗試使用(>>=)或fmap。此外，由於Fix只是newtype，編譯器可能更容易「編譯」Fix的層，因爲它無論如何都只扮演語義角色。

注：我們可以更正式地談論Void和forall a. a如何同構型，以更清楚地看到各類affix和break如何和諧。例如，我們有absurd :: Void -> a作爲absurd (Void v) = absurd v和unabsurd :: (forall a. a) -> Void作爲unabsurd a = a。但是這些有點傻。

來源

2013-07-04 18:04:15

如果您正確定義它們，即'newtype Id a = Id a'和'newtype Fix f = Fix（f（Fix f））'，然後在'let x = Fix（Id x）'後，'x'爲'undefined'（如預期的那樣：'fix id =⊥'，因爲'Fix'和'Id'（構造函數）都是嚴格的。 –

有一個很深的'簡單'連接。

這是adjoint functor theorem的結果，左邊的伴侶保留了初始對象：L 0 ≅ 0。

明確地說，Free f是從一個類別到它的F-代數的一個函子（Free f是一個健忘的函子的左邊，而另一個方向是圓的）。在Hask工作我們最初的代數是Void

Free f Void ≅ 0

和F-代數的類別的初始代數Fix f：Free f Void ≅ Fix f

import Data.Void 
import Control.Monad.Free 

free2fix :: Functor f => Free f Void -> Fix f 
free2fix (Pure void) = absurd void 
free2fix (Free body) = Fix (free2fix <$> body) 

fixToFree :: Functor f => Fix f -> Free f Void 
fixToFree (Fix body) = Free (fixToFree <$> body)

同樣，右伴隨矩陣（Cofree f，從算符Hask至F- co代數）保留最終目標：R 1 ≅ 1。

在Hask這是單位：()和F-的最終目標共同代數也Fix f（他們Hask重合），所以我們得到：Cofree f() ≅ Fix f

import Control.Comonad.Cofree 

cofree2fix :: Functor f => Cofree f() -> Fix f 
cofree2fix (() :< body) = Fix (cofree2fix <$> body) 

fixToCofree :: Functor f => Fix f -> Cofree f() 
fixToCofree (Fix body) =() :< (fixToCofree <$> body)

看看這些定義有多相似！

newtype Fix f 
    = Fix (f (Fix f))

Fix f是Free f沒有變數。

data Free f a 
    = Pure a 
    | Free (f (Free f a))

Fix f是Cofree f虛擬值。

data Cofree f a 
    = a <: f (Cofree f a)

來源

2017-04-04 09:21:37

函子自由單子和固定點之間的區別？

回答

相關問題