由它的類型

Question

一個Haskell的類型系統的有趣特性（*）確定的函數的作用是，有時你可以告訴究竟什麼功能並僅基於其類型簽名（假設沒有unsafe IO黑暗魔法invloved）。

例如，對於類型簽名a -> a任何函數必須是恆等函數，和(a,b) -> a類型的任何功能等同於fst。在某些情況下，您無法完全確定功能：類型爲a -> Int的不同可能功能有無數種，但它們都是常數 - 它們都忽略第一個參數。

我覺得這個屬性很迷人，但我懷疑它只適用於「微不足道」的功能，如id和const。我對麼？

而且，在這裏我的推理只是基於直覺 - 例如，在a -> a，我們「一無所知」關於a（而不是約束的功能，如Num a => a -> a），所以「不能做什麼」與它以外的其他沒有變化。有沒有正式的方法來處理這種扣除？

_{*我知道Haskell的類型系統是基於辛德米爾納型系統上，但我不熟悉它足以承擔任何有關它}

Answer 1

你是指這個概念是已知作爲parametricity。通過類型的通用量化提供了參數多態性和「統一性」屬性，直觀地表明「我們對a」a「forall a. a -> a」沒有任何瞭解，所以除了不改變它之外，「除了它什麼都做不了」。什麼均勻性等級說是一種f :: [a] -> [a]不依賴於a類型，或者更準確地說，取決於它均勻：一切皆有一個「不」的[a]必須是所有選擇「可行」的a。 Wadler使用它來顯示映射列表中的值，然後對列表進行置換，相當於先置換後映射。

正規的方式來處理這些直覺給出的，例如， 菲利普·沃德勒的Theorems for Free，涉及類型和關係之間的同構（其實部分等價關係的類別劃分，每（按的））這表明這種一致性是該類別的普遍性特徵。

參數性的一個有趣的結果是，你可以去「雙向」：從類型到關於該類型的定理，以及從類型到該類型的居民。瓦德爾的自由定理是前者的一個例子，並且一個定理證明者（類型的居民是該類型的「定理」的「證明」）是一個例子，後者是一個例子。