線性類型如何防止「重複」的這種實現？

Question

我最近閱讀the post on Tweag.IO關於線性類型是一個有用的工具，用於表示僅使用（精確地）一次的參數。他們提出了下面的例子：

dup :: a ⊸ (a,a) 
dup x = (x,x) 

現在，也許我誤解的想法，但爲什麼不能用這個來回避：

dup' :: a ⊸ (a,a) 
dup' x = (y,y) 
    where 
    y = x 

文章特別提到參數。這是否擴展到函數中的所有綁定？

Answer 1

我覺得這篇文章幾乎沒有給出底層語義的解釋 - 只是一個例子說明如何使用這樣的技術。公平地說，這可能是博客文章的一種很好的格式。

，您可以查看x ⊸ y爲1 x -> y的同義詞是常規的箭頭，它的域名是1 x它說變量a :: 1 x使用一次。通過類型推斷，在第二個示例中，y獲取推斷類型1 a，因爲y = x和x :: 1 a。這延伸到所有自然數和無窮大。此外，常規箭頭x -> y可以被讀作ω x -> y，其中ω是無窮大。

您鏈接的paper正確提供了語義。見第3.1節，圖。 2 - 對應於let的打字規則。標準分型判斷x : T推廣到x :_{q} T（即q應該是下標）。在現有的Haskell類型語義中，一個術語用其類型進行註釋。在對類型系統的建議擴展中，一個術語是用它的類型和它的多樣性來標註的。

但是，請注意，在該文件中，let構造總是在let-bound變量上包含顯式類型簽名。用這篇論文的語法，你的第二個程序（甚至大多數Haskell程序！）甚至在語法上都是無效的。但我聲稱（沒有證據），不難看出如何將這種類型系統推廣到讓人想起當前Haskell類型系統的類型系統。請參閱GHC trac上的提案，以獲取更多細節。