確定函數式編程中函數的類型

Question

以下等式是用Miranda語法編寫的，但由於Miranda和Haskell之間的相似性，我期望Haskell程序員應該理解它！

如果定義了以下功能：

rc v g i = g (v:i) 
rn x = x 
rh g = hd (g []) 


f [] y = y 
f (x:xs) y = f xs (rc x y) 

g [] y = y 
g (x:xs) y = g xs (x:y) 

你如何制定出的功能類型？我想我明白如何解決f，g和rn問題，但我對部分應用程序部分感到困惑。

RN將是* - > *（或任何東西 - >什麼，我認爲這是一個 - 在Haskell>一個）

對於f和g，是函數類型都[*] - > * - > *？

我不確定如何處理尋找rc和rh的類型。在rc中，g被部分應用於變量i - 所以我猜測這限制了我的類型[*]。 rc和g在rc的定義中應用了什麼順序？ g是否應用於i，然後將得到的函數用作rc的參數？還是rc需要3個獨立的v，g和i參數？我真的很困惑..任何幫助將不勝感激！多謝你們。

對不起忘了補充一點，HD是列表的標準頭功能，並定義爲：

hd :: [*] -> * 
hd (a:x) = a 
hd [] = error "hd []" 

Answer 1

類型是從什麼是已知的類型和表現形式是如何在定義中使用的推斷。

讓我們開始在頂部，

rc v g i = g (v : i) 

所以rc :: a -> b -> c -> d，我們必須看看有什麼可以發現關於a, b, c和d。在右側，出現(v : i)，因此使用v :: a時，我們看到i :: [a],c = [a]。然後g應用於v : i，所以g :: [a] -> d，乾脆，

rc :: a -> ([a] -> d) -> [a] -> d 

rn x = x意味着有上參數類型的rn沒有約束，它的返回類型是一樣的，rn :: a -> a。

rh g = hd (g []) 

由於rh的說法g被施加到在RHS空列表，它必須有類型[a] -> b，可能更多的信息有關a或b如下。事實上，g []是hd在RHS，所以g [] :: [c]和g :: [a] -> [c]的說法，因此

rh :: ([a] -> [c]) -> c 

下一頁

f [] y = y 
f (x:xs) y = f xs (rc x y) 

第一個參數是一個列表，如果是空的，結果是第二個參數，所以f :: [a] -> b -> b從第一個方程得出。現在，在第二個方程中，在RHS上，f的第二個參數是rc x y，因此rc x y必須與y具有相同的類型，我們將其稱爲b。但是

rc :: a -> ([a] -> d) -> [a] -> d 

，所以b = [a] -> d。因此

f :: [a] -> ([a] -> d) -> [a] -> d 

最後

g [] y = y 
g (x:xs) y = g xs (x:y) 

從第一個方程推導出g :: [a] -> b -> b。從第二個，我們推斷b = [a]，因爲我們採取g的第一個參數和缺點它的第二個頭部，從而

g :: [a] -> [a] -> [a] 

Answer 2

我要使用Haskell語法來寫的類型。

rc v g i = g (v:i) 

這裏rc有三個參數，所以它的類型將會像a -> b -> c -> d。 v:i必須是與v和i相同類型的元素列表，因此v :: a和i :: [a]。 g應用於該列表，以便g :: [a] -> d。 如果你把所有的東西放在一起，你會得到rc :: a -> ([a] -> d) -> [a] -> d。

正如你已經想出rn :: a -> a，因爲它只是身份。

我不知道您在rh中使用的hd函數的類型，所以我會跳過它。

f [] y = y 
f (x:xs) y = f xs (rc x y) 

這裏f有兩個參數，所以它的類型將會像a -> b -> c。 從第一種情況我們可以推斷出b == c，因爲我們返回y，並且第一個參數是一個列表。 現在我們知道f :: [a'] -> b -> b。 在第二種情況下通知如何x和y在輸入給予rc：y必須是一個函數[a'] -> d，和rc x y :: a' -> d（即必須也y的類型，因爲它是作爲它的f秒參數傳遞）。 最後，我們可以說f :: [a'] -> ([a'] -> d) -> ([a'] -> d)。由於->是正確關聯的，因此相當於[a'] -> ([a'] -> d) -> [a'] -> d。

你可以用同樣的方式推理其餘的。