给定一个类型，确定你是否可以编写一个总的、终止 Haskell 函数。
对于像Int -> Int 这样的类型，我们知道有限精度整数类型 Int 至少覆盖了[-2^29, 2^29-1] 的范围，因此我们可以从 Int 到 Int 的映射是有限的，所以我们可以写出一个总数，终止函数。
例如，给定以下类型：(a -> b) -> (b -> c) -> (a -> c)，我如何确定我们是否可以编写一个总终止函数来使用该类型作为函数签名？或者这个类型(a -> c) -> ((a, b) -> c)。
非常感谢您通过此问题获得指导！这是一个家庭作业问题，所以我只是寻求指导。
【问题讨论】：
部分答案：
对于有限数据类型，例如您提到的Int 或Bool（我猜所有的 Bounded 都可以包含在内）。那么是的，你可以提供一个完整的功能：
如果您有时间了解Int 的所有案例：
negative :: Int -> Int
negative 0 = 0
negative 1 = -1
negative 2 = -2
negative 3 = -3
...............
...............
negative -1 = 1
negative -2 = 2
...
...
...
直到您涵盖所有案例...这只是一个示例。
Bool 更明显一点，你可以：
negative :: Bool -> Bool
negative False = True
negative True = False
但是，对于带有函数的函数，它们被称为Uncontable set，所以你可以提供所有可能的函数组合，所以它永远不会结束，你总会找到另一个“层次”的函数函数，它是比 Nats 设置的“更大的无限”。
主要问题：
在给定类型的情况下，如何确定是否可以编写一个总的、终止 Haskell 函数？
(a -> b) -> (b -> c) -> (a -> c) 和(a -> c) -> ((a, b) -> c) 也许您可以提供一个。
但是呢：
(a -> b -> c -> d -> e) -> (b -> c) -> (a -> c) -> (d -> e)
我只能肯定地说，你不能保证你会找到至少一个for all所有类型至少一个的组合。但是@Jon Purdy 很好地回答了如何
【讨论】：
给定：
(a -> b) -> (b -> c) -> (a -> c)
通过 Curry-Howard 对应关系，我们知道这不一定是部分——将 -> 解释为逻辑含义，将乘积类型解释为 AND，将 sum 类型解释为 OR——我们发现它形成了一个重言式.但是为了找到一个实现并知道它是全部，我们需要实际找到证明：
(a → b) → (b → c) → a → c
-- ~~~~~~~~~~~~~~~~~~~~~~~~~
-- currying
-- ~~~~~~~~~~~~~~~~~~~~~~~~~
(a → b) ∧ (b → c) → a → c
-- ~~~~~~~~~~~~~~~
-- currying
-- ~~~~~~~~~~~~~~~
(a → b) ∧ (b → c) ∧ a → c
-- ~~~~~~~~~~~~~~~~~
-- commutativity of AND
-- ~~~~~~~~~~~~~~~~~
(b → c) ∧ (a → b) ∧ a → c
-- ~~~~~~~~~~~
-- modus ponens
-- ~
(b → c) ∧ b → c
-- ~~~~~~~~~~~
-- modus ponens
-- ~
c → c
-- ~~~~~
-- reflexivity of implication
-- ~
1
（这是一个假设的三段论。）
我们可以使用这个证明来实现一个实现——跳过这里的柯里化步骤，并且 modus ponens 对应于函数应用：
f ab bc a = bc (ab a)
(a -> c) -> ((a, b) -> c) 的参数与将(a, b) 解释为a ∧ b（逻辑与）类似。
【讨论】：