haskell - 类型正确的功能可以不适用吗？ ( haskell )

Question

我有一个函数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 正确使用。

这个练习让我想到了这个问题；具有正确类型的功能可以不适用吗？
我的直觉使我相信这是错误的，并且任何具有有效类型的函数都存在适​​用的输入。有证据吗？

Answer 1

这是一个简单的证明，证明函数可能不适用(不考虑底部)

data Never = Never Never

justTryIt :: Never -> ()
justTryIt _ = ()

但是您的功能适用

main = print $ foo (\c -> c ()) 3

那么那个 lambda 的类型是什么？

g :: (() -> a) -> a
g = \c -> c ()

重点是您不需要以下功能

g :: (a -> b) -> c

这是无人居住的(iGnOrInG 底部)。类型签名只是说您可以采用一个函数，其中所有 3 个类型(forall a b c.)都可以变化。 IE 这同样适用

g :: (Int -> String) -> Bool
g f = null $ f 3

main = print $ foo g "so concrete"