Gor*_*ato 7 haskell type-inference
我有一个函数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 正确使用。
这个练习让我想到了这个问题；类型正确的函数会不适用吗？我的直觉使我相信这是错误的，并且对于具有有效类型的任何函数都存在适用的输入。有证据吗？
这是一个函数可能不适用的简单证明（不考虑底部）
data Never = Never Never
justTryIt :: Never -> ()
justTryIt _ = ()
但是你的功能是适用的
main = print $ foo (\c -> c ()) 3
那么那个 lambda 的类型是什么？
g :: (() -> a) -> a
g = \c -> c ()
重点是你不需要一个函数
g :: (a -> b) -> c
这是无人居住的（忽略底部）。类型签名只是说您可以采用一个函数，其中所有 3 种类型（forall ab c.）都可以变化。IE 这也同样有效
g :: (Int -> String) -> Bool
g f = null $ f 3
main = print $ foo g "so concrete"
类型的函数p1 -> p2是不可能写出来的；这基本上是说“给定任何可能的类型，我可以给你任何其他可能的类型”。祝你好运！
由于(p1 -> p2) -> t类似的原因，该类型是不可能的。然而，(p1 -> p2) -> Bool很有可能：
f :: (p1 -> p2) -> Bool
f x = True
您可以为各种类型的选择编写类似的函数t。（你不能做的是编写一个可以以某种方式从无到有返回任何可能t的函数。）
更一般地说，每个可实现的函数都可以成功调用吗？这是一个有趣的问题。我不确定答案是什么。我很想知道！
编辑：考虑一下……每个可实现函数的类型签名都可以解释为定理（并且函数的实现在某种意义上是该定理的“证明”）。将另一个函数作为输入的函数就像“如果另一个定理为真，则该定理为真”。因此，如果您能提出“如果 Y 为真，则 X 为真”的证明，其中 Y 肯定为假……那么您就有了永远无法调用的可实现函数。
所有这些都令人愉快地忽略了真正的 Haskell 有几种方法可以打破类型系统并绕过这些好的结果。例如，函数error "banana"具有类型a（即，任何可能的类型）。所以在这种“欺骗”的意义上，所有的 Haskell 函数都是可调用的。