Какое обоснование для типа f x = f x в Haskell есть?

Question

Haskell дает f x = f x тип t1 -> t, но может ли кто-нибудь объяснить почему?

И возможно ли, чтобы любая другая, неэквивалентная функция имела такой же тип?

Answer 1

Хорошо, начиная с определения функции f x = f x, давайте посмотрим, что мы можем вывести о типе f.

Начните с полностью неопределенной переменной типа, a. Можем ли мы вывести более того? Да, мы замечаем, что f является функцией, принимающей один аргумент, поэтому мы можем изменить a на функцию между двумя неизвестными переменными типа, которые мы назовем b -> c. Независимо от типа b обозначает тип аргумента x, и любой тип c должен быть типом правой части определения.

Что мы можем понять о правой части? Ну, у нас есть f, который является рекурсивной ссылкой на функцию, которую мы определяем, поэтому ее тип по-прежнему b -> c, где обе переменные типа те же, что и для определения f. У нас также есть x, который является переменной в определении f и имеет тип b. Применение f к x проверяет тип, потому что они используют один и тот же неизвестный тип b, а результат c.

В этот момент все подходит друг другу и без каких-либо ограничений, мы можем сделать переменные типа «официальными», что приведет к окончательному типу b -> c, где обе переменные являются обычными, неявно универсальными квантованными переменными типа в Haskell.

Другими словами, f - это функция, которая принимает аргумент любого типа и возвращает значение любого типа. Как он может вернуть любой возможный тип? Он не может, и мы можем заметить, что его оценка порождает только бесконечную рекурсию.

По той же причине любая функция с одним и тем же типом будет «эквивалентной» в смысле никогда не возвращаться при оценке.

Еще более прямой вариант, чтобы удалить аргумент целиком:

foo :: a 
foo = foo 

... который также квантор всеобщности и представляет собой значение любого типа. Это в значительной степени эквивалентно undefined.

Answer 2

f x = undefined 

имеет (альфа) эквивалентный тип f :: t -> a.

---

Если вам интересно, система типов Haskell является производным от Hindley–Milner. Неофициально, typechecker начинает с самых разрешительных типов для всего и унифицирует различные ограничения до тех пор, пока что остается неизменным (или нет). В этом случае наиболее общим типом является f :: t1 -> t, и никаких дополнительных ограничений нет.

Сравнить с

f x = f (f x) 

который выведенный тип f :: t -> t, благодаря унификации типов аргумента f на LHS и аргумент к внешней f на РИТ.