haskell - 由两个给定函数组成的函数的类型和定义

Question

我被要求为 s k k 的结果写出最简单的定义。 ， 在哪里

s = \ f g x -> f x (g x)
s :: (t1 -> t2 -> t3) -> (t1 -> t2) -> t1 -> t3
k = \ x y -> x
k :: p1 -> p2 -> p1

写作 :t s k k在终端给出: t -> t .
我认为 s有两个功能 - f和 g .在哪里 f需要 t1和 t2作为输入和返回 t3 .功能 g需要 t1作为输入并返回 t2 , 和 x是 t1 .为什么是 t3返回类型？
我想我理解函数 k , 你在哪里 x和 y作为输入和 x 的类型是输出。在理解这两个函数如何协同工作形成 s k k 时，是否有一种通用方法？ .
我也尝试一步一步输入 :t s k , 给出 (t3 -> t2) -> t3 -> t3 ，但是，这对我没有太大帮助 :) 有人可以向 Haskell 的新手解释一下吗？

Answer 1

如果 fun :: a1 -> b和 arg :: a2 ，然后是应用程序 fun arg :: b和 a1 ~ a2 ( a1 等于 a2 )。s k k与 (s k) k 相同因为函数应用程序关联到左侧。所以我们有一个应用程序s k :

s   :: (t1 -> t2 -> t3) -> (t1 -> t2) -> t1 -> t3
k   :: (p1 -> p2 -> p1)

s k ::                     (t1 -> t2) -> t1 -> t3

p1 ~ t1
p2 ~ t2
p1 ~ t3

请注意 p1 ~ t1和 p1 ~ t3 ，因此 t1 ~ t3 :

s k ::                     (t1 -> t2) -> t1 -> t1

在应用程序 (s k) k ，类似的事情发生；我将使用素数重命名类型变量 '表示这是 k 的不同实例化的类型:

(s k)   :: (t1  -> t2        ) -> t1 -> t1
      k :: (p1' -> p2' -> p1')

(s k) k ::                        t1 -> t1

t1 ~ p1'
t2 ~ p2' -> p1'

请注意，当 t1 -> t2与 p1' -> p2' -> p1' 统一, 等于 p1' -> (p2' -> p1')因为函数类型是右关联的， t2等同于函数类型 p2' -> p1' .
结果整个表达式的类型为 t1 -> t1 , 或 forall t1. t1 -> t1与 ExplicitForAll .即使不知道这里的术语，也只有一个 forall a. a -> a 类型的函数(总计) ，即 id .确实 s k k只是实现恒等函数的一种迂回方式，因为对于任何 X我们给它，它返回 X :

s k k X
(\ f g x -> f x (g x)) k k X
(\ g x -> k x (g x)) k X
(\ x -> k x (k x)) X
k X (k X)
(\ x y -> x) X (k X)
(\ y -> X) (k X)
X

第一个 k选择 X ，以及 k 的第二次申请被忽略。这就是为什么第二次使用 k 的类型变量都没有的原因。 ( p1' 和 p2' )出现在结果类型中。