Haskell неподвижная точка подписи

Question

Что такое подпись следующей функции Haskell:

fix f = f (fix f) 

а) ((а-> Ь) -> а-> Ь) -> а-> б

б) подписи не могут быть синтезированы

с) (а-> а) -> а

Спасибо!

Answer 1

Этот вопрос выглядит как домашнее задание/тестовый вопрос. Я порекомендую вам найти решение самостоятельно:

Сначала у вас, вероятно, установлен GHC, поэтому вы можете запустить ghci реплика haskell.

a section in GHC users' guide about GHCi. Но это довольно долго.

Если вы запускаете GHCI вы получите подсказку, где вы можете ввести Haskell выражения:

Prelude> 1 + 1 
2 
Prelude> map (\x -> x + x) [1, 2, 3] 
[2,4,6] 

Вы также можете связать выражение с именами, и определить функции:

Prelude> let fix f = f (fix f) 

И одна из самых мощных функций - попросить тип выражения:

Prelude> :t map (\x -> x + x) 
map (\x -> x + x) :: Num b => [b] -> [b] 
Prelude> :t fix 
... output omitted 

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

Answer 2

Совершенно другой подход: поиск решения посредством рассуждений.

Правая рука

f (fix f) 

так f имеет тип a -> b для некоторых типов a и b, так как f функция.

Иными словами, значение f (fix f) имеет тип b, а fix f имеет тип a.

Так как, по определению,

fix f = f (fix f) 

fix f должны иметь тот же тип, как f (fix f), т.е. b.

Мы уже говорили, что a является тип fix f, так a и b должны быть того же типа.

Назовем его t, чтобы все было в порядке.

Так f : t -> t, поскольку a и b были такого же типа t.
Мы знаем, что fix f имеет тип b, который мы переименовали в t.

Ввод f : t -> t и fix f : t вместе мы получаем

fix : (t -> t) -> t 

, который является альтернативой с).

---

В сторону: если мы подставим a -> b для t мы получаем

((a -> b) -> (a -> b)) -> (a -> b) 

или, так как стрелка правоассоциативным на:

((a -> b) -> a -> b) -> a -> b 

это именно ответ в).
Итак, а) почти правильно, но недостаточно общего.