瞭解Monad'>> ='函數中的所有內容嗎？

Question

繼this的答案，我已經實現了一個通用的升降功能在我的程序：

liftTupe :: (x -> c x) -> (a, b) -> (c a, c b) --This will error 
liftTuple :: (forall x. x -> c x) -> (a, b) -> (c a, c b) 

我明白了，在這種情況下，forall正在使x是任何類型的（[]，Maybe等。） 。

我現在正在研究中的單子的>>=定義：

class Applicative m => Monad m where 
    (>>=) :: forall a b. m a -> (a -> m b) -> m b 

我無法理解這樣的forall在函數定義中的作用是什麼？與liftTuple不同，它不是綁定到特定功能（x -> c x）？

Answer 1

基本上，當您不使用forall時，所有類型在函數定義中都是全局的，這意味着它們都是在函數被調用時推導出來的。使用forall，您可以放棄以x作爲自身函數的功能。

所以在第一個你有一個函數，它接受x並給出c x，那麼你有a和b一個元組，你期望與c a和c b的元組。既然你已經說第一個函數接受了x，你可以讓x變成與a一樣，但它不會是b，那麼因爲x是爲整個聲明定義的。所以你不能使該功能同時接受a和b。

但是，在第二種情況下，x範圍僅限於功能爲x。我們基本上是說，有一個功能需要一些東西，並使得它具有某種東西，它可以是任何類型的東西。這使我們能夠首先向其提供a，然後b，它將起作用。 x現在不一定是單獨的東西。

您在Monad定義中看到的是「ExplicitForAll」語言擴展。有這個擴展上Haskell Prime描述

ExplicitForAll允許使用關鍵字「FORALL」，明確規定一類是在其遊離型變量多態。它不允許寫入任何不能寫入的類型;它只允許程序員明確說明（當前隱含的）量化。

該語言擴展是純粹的可視化，允許你明確地寫出你以前不能的變量。您可以簡單地省略Monad聲明中的forall a b.，該程序在功能上將保持完全相同。

說，用這個擴展名你可以重寫liftTupe爲forall a b x. (x -> c x) -> (a, b) -> (c a, c b)。定義相同，功能相同，但讀者現在可以清楚地看到，類型變量都定義在最上層。

Answer 2

Haskell類型系統中的所有類型變量都被量化爲forall。但是，GHC可以在許多情況下推斷量化，因此您無需在源代碼中編寫它們。

。例如liftTuple與forall明確的類型是

liftTuple :: forall c a b. (forall x. x -> c x) -> (a, b) -> (c a, c b) 

而對於>>=的情況下是相同的。

Answer 3

你寫的每一個功能隱含普遍超過其類型變量量化：

id :: a -> a   -- this is actually universally quantified over a 
id :: forall a. a -> a 
id x = x 

實際上，你可以打開與ExplicitForall語言編譯此行爲。

該屬性非常有用，因爲它限制了您編寫僅適用於某些類型的代碼。想想id函數可以做什麼：它可以永久返回它的參數或循環。這是它可以做的唯一兩件事情，你可以根據它的類型簽名來判斷。

強制多態函數的所有實例的行爲方式相同，不考慮參數的類型被稱爲parametricity和巴爾託什盧斯基在this博客文章解釋。 TL; DR是：使用參數性，我們可以保證在程序結構中的一些重新排序不會影響它的行爲。對於這種數學上更嚴格的處理，請參閱Philip Wadler的Theorems for free!。

Answer 4

monad定義中的全部內容僅用於使通用量化更加明確。如果你有一個沒有進一步限制的類型變量，它默認是通用的，即可以是任何東西。

因此讓我們來看FORALL的兩種用法之間的差異和Haskell如何可能會看到他們：

隱：

foo :: (x -> f x) -> a -> b -> (f a, f b) 
-- same as 
foo :: forall f x a b . (x -> f x) -> a -> b -> (f a, f b) 
-- our function is applied to a, so x is equal to a 
foo :: forall f x a b . (x ~ a) => (x -> f x) -> a -> b -> (f a, f b) 
-- our function is also applied to b, so x is equal to b 
foo :: forall f x a b . (x ~ a, x ~ b) => (x -> f x) -> a -> b -> (f a, f b) 

嗯哦，（X〜A，X〜b）項要求（a〜b）。這將推斷沒有註釋，但由於我們明確使用不同的類型變量一切都炸了。爲了解決這個問題，我們需要f在我們的函數中保持多態。

標準haskell無法表達這個，所以我們需要rank2types或者rankntypes。我們可以這樣寫：

foo :: (forall x . x -> f x) -> a -> b -> (f a, f b) 

請注意，該函數是函數類型的一部分。這樣它在我們的函數中保持多態，並且我們可以將它應用於不同的類型，而不會造成任何問題！

請注意，我們也可能只是做：

foo :: Monad m => a -> b -> (m a, m b) 
foo a b = (return a, return b)