驗證lambda表達式的

Question

我需要驗證的lambda表達式類型類型：

我的方法給我：

我試着在Haskell來定義它（上擁抱），如這樣的：

h= \f x -> f (f x) 

當我致電：類型comamnd它給了我：

(a -> a) -> a -> a 

是否在Haskell中正確定義了mi函數？或者我的方法給了我一個錯誤的結果？

Answer 1

注意f被調用與兩個x和f x作爲其參數，這立即意味着x和類型的f x類型必須是相同的[1]。繼續這個論點，我們看到x是f的輸入，而f x是f的輸出，所以f的輸入和輸出必須是相同的[2]。

最後，我們檢查拉姆達術語

\f x -> f (f x) 

它具有兩個輸入，f（函數），並x，並將其返回任何的f返回類型爲[3]。把這些信息放在一起，我們有

(a -> b) -> c -> d 

where: 

    b ~ c  by [1] 
    a ~ b  by [2] 
    d ~ b  by [3] 

因此這哈斯克爾推斷類型正確

h :: (a -> a) -> a -> a 
h f x = f (f x) 

Answer 2

你的Haskell命令很好。

雖然您的類型推斷不正確。由於您致電f x，因此輸入類型f應該與f的輸出類型相同，因爲您在結果(f x)上致電f，因此x自變量的類型應該與輸入類型f相一致。

Answer 3

類型(a -> b) -> (c -> d)相當於在haskells類型系統中的(a -> b) -> c -> d。您還需要考慮，如果x已鍵入a，並且f x具有類型b，則f具有類型a -> b。所以讓y = f x。那麼f y === f (f x)的類型是什麼？