1

这个问题取自考试。我不知道该怎么做。:-(

问题：举一个 haskell 或 ml 函数的例子，它的类型是

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

怎么做？

4

3 回答 3

7

什么有意义的功能可以有类型mystery :: ( a -> b ) -> ( c -> a ) -> c -> b？

看看能有什么

mystery f g x

是？

它需要处理三件事，

  • 一个x类型的值c，
  • g一种类型的函数c -> a和
  • ftype 的一种功能a -> b。

它应该产生一个类型的值b。

唯一与函数有关的参数b是函数f，因此结果必须是f ???。

这里的论点是f什么？它必须具有 type ，并且从给定参数（忽略底部，，， ）a产生该类型值的唯一方法是应用于某些东西，所以它必须是undefinederror "foo"g

mystery f g x = f (g ??)

但是可以g应用于什么？那必须是 type 的值c。除了底部之外，唯一c可以从参数构造的类型值是x，所以

mystery f g x = f (g x)

必须是函数组合（或未定义）。

于 2012-12-31T05:27:57.380 回答
4

到目前为止，其他答案实际上并未显示一般执行此操作的逻辑过程。我也不会 100% 详细地展示它，但我会举一个例子。

对此的“深层”技巧是找到给定类型的函数等同于证明逻辑定理。使用Lemmon 系统 L的一种形式（在一些初级逻辑课程中使用的一种更友好的自然演绎形式），您的示例将如下所示：

Theorem:  ??? :: (a -> b) -> (c -> a) -> c -> b

1.                 f :: a -> b  (aux. assumption)
2.                 g :: c -> a  (aux. assumption)
3.                 x :: c       (aux. assumption)
4.               g x :: a       (2, 3, -> elim; assumes 2, 3)
5.           f (g x) :: b       (1, 4, -> elim; assumes 1, 2, 3)
6.     \x -> f (g x) :: c -> b  (3, 4, -> intro; discharges 3, assumes 1, 2)

7.   \g x -> f (g x) :: (c -> a) -> c -> b
                        (2, 6, -> intro; discharges 2, assumes 1)

8. \f g x -> f (g x) :: (a -> b) -> (c -> a) -> c -> b  
                        (1, 7, -> intro; discharges 1)

这里的想法是函数式编程语言和逻辑之间存在紧密的对应关系，例如：

  1. 类型对应于逻辑命题
  2. 函数定义对应逻辑证明
  3. 逻辑证明规则对应于如何构造编程语言表达式的规则。

因此，“辅助假设”逻辑证明规则（步骤 1-3）对应于引入一个新的自由变量。隐含消除规则（步骤 4-5，又名“作案方式”）对应于函数应用。蕴涵引入规则（步骤 6-8，又名“假设推理”）对应于 lambda 抽象。解除辅助假设的概念对应于绑定自由变量。没有前提的证明的概念对应于没有自由变量的表达式的概念。

于 2012-12-31T20:05:17.940 回答
2

该函数是函数组合运算符，通过在 Hoogle 中键入函数的类型，您可以找到：http ://www.haskell.org/hoogle/?hoogle=%28+a+-%3E+b+%29+- %3E+%28+c+-%3E+a+%29+-%3E+c+-%3E+b++

然后您可以单击以显示源：

(.)    :: (b -> c) -> (a -> b) -> a -> c
(.) f g = \x -> f (g x)
于 2012-12-31T05:21:53.043 回答