從類型寫入滿足類型的函數

Question

此問題取自考試。我不知道該怎麼做。 :-(

問題：給一個Haskell或毫升功能，其類型爲

（一 - > B） - 的例子>（C - >一） - >Ç - >乙

如何做到這一點

Answer 1

什麼有意義的函數可以有類型mystery :: (a -> b) -> (c -> a) -> c -> b？

讓我們來看看，有什麼能

mystery f g x 

是什麼？

它有三個方面的工作，

• 一個值c類型的x，
• 一個功能c -> a類型和
• 一個功能a -> b類型的f的g。

它應產生一個值爲b的值。

與b有任何關係的唯一理由是函數f，所以結果必須是f ???。

f這裏的參數是什麼？它必須有a類型，並從給定的參數產生該類型的值的唯一途徑（忽略底部，undefined，error "foo"）正在申請g的東西，所以它必須是

mystery f g x = f (g ??) 

但什麼事情g被應用於？這必須是c類型的值。除了底部，可從參數來構造c類型的唯一值是x，所以

mystery f g x = f (g x) 

必須是功能組合物（或未定義）。

Answer 2

該函數的功能是合成運算，並通過鍵入函數的類型分爲Hoogle你會發現說出來：http://www.haskell.org/hoogle/?hoogle=%28+a+-%3E+b+%29+-%3E+%28+c+-%3E+a+%29+-%3E+c+-%3E+b++

然後，您可以點擊顯示來源：

(.) :: (b -> c) -> (a -> b) -> a -> c 
(.) f g = \x -> f (g x) 

Answer 3

到目前爲止的其他答案實際上並沒有顯示通常這樣做的邏輯程序。我不會以100％的細節展示它，但我會舉一個例子。

這個「深層次」的技巧是找到給定類型的函數是相當於證明了一個邏輯定理。使用Lemmon's System L形式（的natural deduction在一些開始的邏輯課程使用友好的形式），你的例子會是這樣的：

Theorem: ??? :: (a -> b) -> (c -> a) -> c -> b 

1.     f :: a -> b (aux. assumption) 
2.     g :: c -> a (aux. assumption) 
3.     x :: c  (aux. assumption) 
4.    g x :: a  (2, 3, -> elim; assumes 2, 3) 
5.   f (g x) :: b  (1, 4, -> elim; assumes 1, 2, 3) 
6.  \x -> f (g x) :: c -> b (3, 4, -> intro; discharges 3, assumes 1, 2) 

7. \g x -> f (g x) :: (c -> a) -> c -> b 
         (2, 6, -> intro; discharges 2, assumes 1) 

8. \f g x -> f (g x) :: (a -> b) -> (c -> a) -> c -> b 
         (1, 7, -> intro; discharges 1) 

這裏的想法是，there is a tight correspondence between functional programming languages and logic，使得：

1. 類型對應於邏輯命題
2. 函數定義對應於邏輯證明
3. 邏輯證明規則對應於關於如何構造編程語言表達式的規則。

所以「輔助假設」邏輯證明規則（步驟1-3）對應於引入一個新的自由變量。隱含消除規則（步驟4-5，a.k.a.「modus ponens」）對應於功能應用。蘊涵引入規則（步驟6-8，又名「假設推理」）對應於拉姆達抽象。排除輔助假設的概念對應於約束自由變量。無前提證明的概念對應於沒有自由變量的表達式的概念。