类型正确的功能可以不适用吗？ （哈斯克尔）

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"

Answer 2

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 函数都是可调用的。