Хаскелл: пример функции типа а → а, кроме тождества

Ответ 1

Это невозможно без использования undefined в качестве упоминаемого другого комментатора. Докажем это контрпример. Предположим, что существует такая функция:

f :: a -> a

Когда вы говорите, что это не то же самое, что id, это означает, что вы не можете определить:

f x = x

Однако рассмотрим случай, когда a является типом ():

f () = ...

Единственный возможный результат f может быть возвращен, будет (), но это будет та же реализация, что и id, поэтому противоречие.

Более сложный и строгий ответ заключается в том, чтобы показать, что тип a -> a должен быть изоморфен (). Когда мы говорим, что два типа a и b являются изоморфными, это означает, что мы можем определить две функции:

fw :: a -> b
bw :: b -> a

... такое, что:

fw . bw = id
bw . fw = id

Мы можем легко сделать это, когда первый тип a -> a, а второй тип ():

fw :: (forall a . a -> a) -> ()
fw f = f ()

bw :: () -> (forall a . a -> a)
bw () x = x

Тогда мы можем доказать, что:

fw . bw
= \() -> fw (bw ())
= \() -> fw (\x -> x)
= \() -> (\x -> x) ()
= \() -> ()
= id

bw . fw
= \f -> bw (fw f)
-- For this to type-check, the type of (fw f) must be ()
-- Therefore, f must be `id`
= \f -> id
= \f -> f
= id

Когда вы доказываете, что два типа изоморфны, вы знаете, что если один тип заселен конечным числом элементов, то и другой. Так как тип () населен ровно одним значением:

data () = ()

Это означает, что тип (forall a . a -> a) также должен быть заселен ровно одним значением, что как раз и является реализацией для id.

Изменить: некоторые люди прокомментировали, что доказательство изоморфизма недостаточно строго, поэтому я буду ссылаться на лемму Йонеды, которая при переводе в Хаскелл говорит, что для любого функтора f:

(forall b . (a -> b) -> f b) ~ f a

Где ~ означает, что (forall b . (a -> b) -> f b) изоморфно f a. Если вы выберете функтор Identity, это упростит:

(forall b . (a -> b) -> b) ~ a

... и если вы выберете a = (), это упростит следующее:

(forall b . (() -> b) -> b) ~ ()

Нетрудно доказать, что () -> b изоморфно b:

fw :: (() -> b) -> b
fw f = f ()

bw :: b -> (() -> b)
bw b = \() -> b

fw . bw
= \b -> fw (bw b)
= \b -> fw (\() -> b)
= \b -> (\() -> b) ()
= \b -> b
= id

bw . fw
= \f -> bw (fw f)
= \f -> bw (f ())
= \f -> \() -> f ()
= \f -> f
= id

Таким образом, мы можем затем использовать это, чтобы, наконец, специализировать изоморфизм Ионеды на:

(forall b . b -> b) ~ ()

Говорят, что любая функция типа forall b . b -> b изоморфна (). Лемма Йонеды обеспечивает строгость моего доказательства.

Ответ 2

Позвольте мне сформулировать ответ, в котором подробно рассматривается комментарий dbaupps. Любая функция типа a -> a также приведет к функции типа () -> (), поэтому я сначала рассмотрю эту подзадачу.

Обычная семантика типов и функций Хаскелла будет представлять собой тип как цельный неполный порядок цепочки и функционирует как непрерывные функции. Тип () представлен двумя наборами элементов {⊥,()} с порядком ⊥⊏(). В теории простых множеств из этого множества есть 2 ^ 2 = 4 функции, но только три из них непрерывны:

• f1: ⊥ ↦ ⊥,() ↦ ⊥,
• f2: ⊥ ↦ ⊥,() ↦() и
• f3: ⊥ ↦(),() ↦().

Таким образом, в нашей семантической модели существуют три различные функции типа () -> (). Но какой из них может быть реализован в Haskell? Все они!

• f1 _ = undefined (или f1 x = f1 x)
• f2 x = x (или f2 = id)
• f3 _ = () (или f3 = const ())

Посмотрев на эти определения, вы можете увидеть, что f1 и f2 также могут использоваться для определения функции типа a -> a. Поскольку они уже делают разные вещи на (), они различны. Итак, у нас есть как минимум две разные функции типа a -> a.

В приведенной выше семантической модели существует гораздо больше функций типа a -> a, но они не будут выражены в Haskell (это связано с параметричностью и Wadlers Теоремы бесплатно). Правильное доказательство того, что f1 и f2 - единственные такие функции, кажется, не очень легким, так как это зависит от того, что язык Haskell запрещает (например, отсутствие сопоставления шаблонов по типу аргумента).

Ответ 3

Если вы не хотите использовать undefined или bottom (выражение без конца), буквально нет других функций, удовлетворяющих этому типу.

Это одна из сильных сторон системы типа Haskell. Это позволяет сильно ограничить возможные функции, которые могут проходить через компилятор в те, которые, очевидно, правильны. В качестве крайнего примера см. djinn - он принимает тип и генерирует возможные функции, соответствующие этому типу. Даже для реальных сложных примеров список часто очень короткий.

Ответ 4

Ключевым моментом здесь является понимание того, что мы ничего не знаем о a, особенно у нас нет способа создать новый или преобразовать его в нечто иное. Следовательно, у нас нет выбора, как вернуть его (или нижнее значение). Как только у нас появится дополнительная информация о a (например, привязана к контексту), мы можем сделать с ним более интересные вещи:

f :: Monoid a => a -> a
f _ = mempty

или

f :: Monoid a => a -> a
f x = x `mappend` x `mappend` x

Или, если у вас есть выбор, как в f :: (a, a) -> a, у вас есть две возможные реализации (игнорируя нижние значения снова), но для f :: (a, b) -> a вы вернетесь к одной реализации, которая такая же, как для fst: Хотя для вызова f можно использовать пару одинаковых типов, например f ("x", "y"), вы можете быть уверены, что f ведет себя как fst, потому что в реализации f у вас нет возможности проверить, будут ли оба типа аргументов одинаковыми. Аналогично, существует только одна не-нижняя версия f :: (a -> b) -> a -> b.

Полиморфизм ограничивает степень свободы, потому что вы ничего не знаете о своих аргументах, а в некоторых случаях это сводится к одной недвойной версии.

Ответ 5

Как уже упоминалось, такой общей функции не существует. (Если мы не ограничимся полными функциями, то мы можем населить любой тип на undefined.)

Я попытаюсь дать теоретическое объяснение, основанное на λ-исчислении:

Для простоты ограничимся λ-членами (к которым мы можем перевести любое выражение Хаскелла). Для λ-терма M позвоните A своей голове, если M ≡ A N1 ... Nk и A не является приложением (k также может быть нулевым). Обратите внимание: если M находится в нормальной форме, то A не может быть λ-абстракцией, если k = 0.

Итак, пусть M :: a -> a - λ-член в нормальной форме. Поскольку у нас нет переменных в контексте, M не может быть переменной и не может быть приложением. Если бы это было так, его голова была бы переменной. Итак, M должна быть λ-абстракцией, она должна быть M ≡ λ(x:a).N.

Теперь N должен иметь тип A, формально {x:a}⊢N:a. Если N была λ-абстракцией, ее тип был бы σ -> τ, что невозможно. Если N было прикладной функцией, тогда голова должна была быть переменной, и единственная, которая у нас есть в контексте, - это x. Но поскольку x:a, мы не можем применить x к чему-либо, x P не является пленкой для любого P. Таким образом, единственная возможность заключается в том, что N ≡ x. Итак, M должен быть λ(x:a).x.

_{(Пожалуйста, исправьте мой английский, если это возможно. В частности, я не уверен, как использовать subjunctive право).суб >}