У меня есть функция foo = \f x -> let c = \y -> x in f c
, которую я нашел, чтобы найти:
\forall a,b,r. ((b -> a) -> r) -> a -> r
.
GHCI подтверждает этот тип: foo :: ((p1 -> p2) -> t) -> p2 -> t
Однако я не могу найти подходящую функцию, которая соответствует этим параметрам, так что foo
оценивает.
Я пытался Следующие функции не увенчались успехом:
bu :: Num a => ([Char] -> a) -> a
bu x = (x "hello") * 2
ba :: (Fractional a1, Foldable t) => t a2 -> a1
ba x = (fromIntegral (length x) ) / 2
Другой попыткой был выбор следующих функций:
bu :: Num a => ([Char] -> a) -> a -> a
bu x = (+ ((x "hello") * 2))
ba :: (Fractional a1, Foldable t) => t a2 -> a1
ba x = (fromIntegral (length x) ) / 2
Теперь я могу позвонить (bu ba) 4
и получить правильный результат.
Я понимаю, почему они не работают. Кажется, проблема в том, что в первом аргументе (p1 -> p2) -> t)
, t
должна быть функцией, которая принимает аргумент p2
. Однако, как только мы это сделаем, тип этой функции изменится на что-то вроде (a -> a)
и больше не будет корректно использоваться foo.
Это упражнение привело меня к вопросу; может ли функция с правильным типом быть неприменимой? Моя интуиция заставляет меня верить, что это неверно и что для любой функции с допустимым типом существует соответствующий ввод. Есть ли доказательства для этого?