追蹤功能的部分應用類型

Question

我一直在檢查Lens的類型以瞭解它，並且無法找出在那裏部分應用的結果類型導致的類型。

初始型是這樣的：type RefF a b = forall f. Functor f => (b -> f b) -> (a -> f a)

應用於Identity算符上述類型變成這樣：

(b -> Identity b) -> (a -> Identity a) 

它們的修改函數的定義是這樣的：

modify :: RefF a b -> (b -> b) -> a -> a 
modify r m = runIdentity . r (Identity . m) 

我分解上面的定義可以更好地理解它。

從以上，Identity . m類型是b -> Identity b

我甚證實了這一使用typechecker：

check1 :: (b -> b) -> b -> Identity b 
check1 m = Identity . m 

現在，我試着制定的r (Identity . m)類型。這是我心靈空虛的地方。的r (Identity . m)部分應用程序的實際結果似乎是a -> Identity a爲typechecked如下：

check2 :: RefF a b -> (b -> Identity b) -> a -> Identity a 
check2 r che = r che 

一個人怎麼算出這個弱智？當我嘗試部分適用於cher，它似乎並不適合：

The type of `r` is : (b -> Identity b) -> (a -> Identity a) 
The type of `che` is : (b -> Identity b) 

怎樣才能描繪出那的r che部分應用程序是(a -> Identity a)

Answer 1

當我嘗試部分申請車到R，它似乎並不適合：

r具有類型

(b -> Identity b) -> (a -> Identity a) 

這意味着它的第一個參數需要有類型(b -> Identity b)。

che具有類型

(b -> Identity b) 

正如需要r，因此r che將工作和有型(a -> Identity a)。

應用到第三個參數後，假設它已被命名爲arg的modify，這arg具有類型a，r (Identity . m) arg將有Identity a類型，之後應用就可以了runIdentity，結果將具有類型a。

---

type RefF a b = forall f. Functor f => (b -> f b) -> (a -> f a) 

modify :: RefF a b -> (b -> b) -> a -> a 
modify r m = runIdentity . r (Identity . m) 

你可以推斷出modify r m這樣類型：

1. r的類型爲RefF a b，這是(b -> f b) -> (a -> f a)
2. m具有類型b->b
3. Identity具有類型forall a. a -> Identity a，因此Identity . m的類型爲b -> Identity b
4. r (Identity . m)的類型爲a -> Identity a，因爲f必須Identity
5. runIdentity具有類型forall a. Identity a -> a，因此runIdentity . r (Identity . m)具有類型a -> a