id - единственная функция типа a -> a, и
fst единственная функция типа (a,b) -> a. В этих простых случаях это довольно просто видеть. Но в целом, как бы вы это доказали? Что делать, если есть несколько возможных функций одного и того же типа?
В качестве альтернативы, учитывая тип функции, как вы получаете уникальную (если это правда) функцию этого типа?
Изменить: меня особенно интересует, что происходит, когда мы начинаем добавлять ограничения в типы.
Результат, который вы ищете, проистекает из параметричности Рейнольдса, и он был наиболее знаменито продемонстрирован Вадлером в теоремах бесплатно.
Самый элегантный способ доказать основные результаты параметричности, я видел использование понятия "Singleton Type". По существу, учитывая любой ADT
data Nat = Zero | Succ Nat
существует индексированное семейство (также известное как GADT)
data SNat n where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
и мы можем дать семантику нашему языку путем "стирания" всех типов к нетипизированному языку, так что Nat и SNat стирают одно и то же. Затем, по правилам ввода языка
id (x :: SNat n) :: SNat n
SNat n имеет только один житель (его одноэлементный), так как семантика задается стиранием, функции не могут использовать тип своих аргументов, поэтому единственное значение, возвращаемое из id на любом Nat, - это число вы дали это. Этот основной аргумент может быть расширен, чтобы доказать большую часть результатов параметричности и был использован Карлом Крари в Простой метод доказательства результатов параметричности, хотя представленная здесь презентация вдохновлена Камень и Харпер