計算Haskell函數的類型

Question

在Haskell爲週末考試手動計算給定函數的類型時遇到麻煩。

予瞭解的基礎知識，例如：

• IX = X ::噸 - >噸
• KXY = X ::噸 - > T1 - >噸

但是具有麻煩更復雜的問題，例如：

• 2 FX = F（FX）
• sxyz = x z（y z）

任何解釋將不勝感激！

Answer 1

在這兩個例子中，關於函數類型的唯一提示來自觀察正在進行的應用程序。在Haskell應用程序中幾乎沒有任何語法，所以我會更明顯地重寫它們。

two f x = f(f(x)) 
s x y z = x(z)(y(z)) 

---

現在，我們將通過逐步細化發現的類型，這些功能。例如，對於two開始，我們知道，它需要兩個參數，因此必須具有與（更普遍）同意一種類型

two :: a -> b -> c 

我們也知道，上面居然a型變量相當於一個函數因爲f正在應用於x和f(x)。

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

由於f應用於x我們知道這裏a和c必須相同。

two :: (a -> b) -> a -> d 

因爲我們再次申請f其結果f(x)我們知道結果類型必須相同，輸入型

two :: (a -> a) -> a -> b 

最後，調用f的結果是總結果的two所以d還必須等於a

two :: (a -> a) -> a -> a 

這使用了我們在定義中提供的所有信息，並且是與two的定義兼容的最一般類型。

---

我們可以對s做基本相同的處理。我們知道它有3個參數

s :: a -> b -> c -> d 

我們知道，第一和第二個參數是某種功能。我們看到第二個參數應用於單個值，第一個參數應用於兩個值。

s :: (a -> b -> c) -> (d -> e) -> f -> g 

我們也知道，兩者的輸入功能第一是相同的（即，它的每一次z）。這讓我們推斷a，d和f是同一類型的

s :: (a -> b -> c) -> (a -> d) -> a -> e 

我們也知道，調用第二函數的結果是第二個參數的第一個函數，所以b和d必須是相同的。

s :: (a -> b -> c) -> (a -> b) -> a -> e 

最後，要充分應用的第一功能的結果是s如此c和e最終的結果都是一樣

s :: (a -> b -> c) -> (a -> b) -> a -> c 

---

雖然這可能是很多消化和種類模糊不清，需要強調的是我用來解決這個問題的工具都是原始的。實際上，當我看到類型被應用於某些值並因此必須是一定數量參數的函數時，我會引入箭頭(->)，並通過在表達式中跟蹤值來統一類型變量。這些是推斷簡單功能類型的足夠工具，如two和s。

Answer 2

您的two和s就是所謂的高級函數，因爲它們將函數作爲參數。你已經有了識別它們類型的工具，你只需要願意抽象一些。

如果你給出的表達式

f x 

你知道的f類型是a -> b與x :: a和f x :: b。如果你看到

f (f x) 

然後你就可以推斷出的(f x)輸出類型是相同f輸入類型。這意味着a ~ b，所以f :: a -> a和x :: a。如果我們看一下two類型，我們可以推斷，它遵循的模式

two :: s -> t -> u 

但第一個參數two是f，它具有類型a -> a，所以我們可以插上，在作爲

two :: (a -> a) -> t -> u 

而且x是a型的第二個參數，所以我們可以插上，在

two :: (a -> a) -> a -> u 

而返回類型相同返回類型的f (f x)，其中有f返回類型，其中有a返回類型，所以如果我們插上，在我們最終的類型

two :: (a -> a) -> a -> a 

---

對於s，我們可以做類似的操作。我們首先說s如下表格

s :: s -> t -> u -> v 

因爲它有3個參數。表達式(y z)是函數應用，所以y必須具有y :: a -> b類型，其中z :: a。堵在給s：

s :: s -> (a -> b) -> a -> v 

那麼我們來看x z (y z)。由於y z :: b和z :: a，x是兩個參數的函數，第一a型和b類型的第二，與一些不知名的返回類型c，所以我們可以插上，在作爲

s :: (a -> b -> c) -> (a -> b) -> a -> c 

Answer 3

讓我們來看看

two f x = f (f x) 

我們將繼續寫下我們所知道的，使用變量來表示我們不知道的任何東西。我們知道的一些東西是方程式，就像數學中一樣，我們將在方程中取代周圍，直到我們得到一些我們無法做到的事情。

從表達式f x開始。 f是一個函數，它的參數類型是什麼x的類型，所以：正是我只是在前面的句子說

x :: a  -- a is a new variable 
f :: a -> b -- b is a new variable 

這兩個等式說。此外，我們創建的變量b這是應用程序的結果類型：

f x :: b 

現在讓我們進入到f (f x)。所以f參數類型必須是f x類型，這是我們所知道的是b，所以：

f :: b -> c -- c is a new variable 
f (f x) :: c 

但是，當然，一個函數只能有一個類型，我們已經爲f類型：

f :: a -> b -- from above 

這意味着，

a = b 
b = c 

現在，我們已經達到了頂級水準表現。所以，現在讓我們來看看，我們發現與表達共同類型的輸入變量：

f :: a -> b 
x :: a 
f (f x) :: c 

現在，我們去代四周，盡我們所能，以儘可能少的變量可能表達它（但只使用我們推斷出的平等）。我們將盡力根據a完成。

f :: a -> b 
    = a -> a -- because b = a 
x :: a 
f (f x) :: c 
     = b -- because c = b 
     = a -- because b = a 

而且我們有它：

two :: (a -> a) -> a  ->  a 
     ^^^^^^^^^  ^^^^^^^^^ ^^^^^^^^^^^^^^ 
     type of f  type of x type of result 

這比需要更詳細的，因爲我自己重複了很多，這樣你可以看到涉及的推理。有一個有條不紊的方法來做到這一點，但我更喜歡做更像數學，繼續前進，並發現我能做的。有條不紊的方法通常讓我迷失在變數的海洋中（這對於計算機來說很容易，但對我的人類大腦卻很難）。

我希望這有助於。