时间戳

首页 > 解决方案 > 写一个给定类型的总的，终止 Haskell 函数

haskell - 写一个给定类型的总的，终止 Haskell 函数

问题描述

给定一个类型，确定你是否可以编写一个总的、终止的 Haskell 函数。

对于类似 的类型Int -> Int，我们知道有限精度整数类型 Int 至少覆盖范围[-2^29, 2^29-1]，因此我们可以有从 Int 到 Int 的有限多个可能的映射，因此我们可以编写一个总的终止函数。

例如，给定以下类型：(a -> b) -> (b -> c) -> (a -> c)，我如何确定我们是否可以编写一个总终止函数来使用该类型作为函数签名？还是这种类型(a -> c) -> ((a, b) -> c)。

非常感谢通过这个问题的指导！这是一个家庭作业问题，所以我只是寻求指导。

标签： haskelltypes

解决方案

鉴于：

(a -> b) -> (b -> c) -> (a -> c)

我们知道，Curry-Howard 对应关系不一定是部分->的——将产品类型解释为 AND，将 sum 类型解释为 OR——我们发现它形成了一个重言式。但是为了找到一个实现并知道它是 total，我们需要实际找到证明：

   (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

（这是一个假设的三段论。）

我们可以使用这个证明来实现一个实现——跳过这里的柯里化步骤，并使用对应于函数应用的方式：

f ab bc a = bc (ab a)

该论点类似于(a -> c) -> ((a, b) -> c)解释(a, b)为a ∧ b（逻辑与）。

推荐阅读