haskell 函数类型简化 f :: ((b -> a ) -> a -> c ) -> (b -> a ) -> b -> c

Question

只是在寻找这个函数类型的解释，拜托

f x y z = x y (y z)

前奏说的是

f :: ((b -> a) -> a -> c) -> (b -> a) -> b -> c

但我无法使用任何已知方法获得该结果 ¬¬

此致。

Answer 1

呃，那些“手动检查这个表达式”的练习太傻了。我不知道为什么讲师总是给他们布置作业。

在实践中，实际上更相关的是反过来：给定一个类型，找到一个实现。那么让我从那个角度来回答这个问题：你已经知道了

f :: ((b -> a) -> a -> c) -> (b -> a) -> b -> c
--   └──────────────────┘    └──────┘   └─┘

...所以你有三个参数要接受，足够合理地称它们为 x、y 和 z

f x y z = _

您最终在寻找 c，而您唯一可用的 c 是 x

的最终结果

    x :: (b -> a) -> a -> c
    --   └──────┘   └─┘

...需要两个参数

f x y z = x _ _

...类型 b -> a 和 a。让我们看看我们有什么可用的

    y :: b -> a
    z :: b

很好，我们可以直接用y作为第一个参数

f x y z = x y _

对于第二个参数，我们需要一个 a。好吧，z 是一个 b，这是行不通的，但是 y 在给定一个 b 时会产生一个 a，所以我们可以传递 y z 并最终得到

f x y z = x y (y z)

或者我们更喜欢写成 Haskell, f x y = x y . y.

现在反过来说：让我们从 η 简化形式开始

f x y = x y . y

这是一个管道，所以让我们开始给 passing-through 参数起一个名字 p

        x y . y :: p -> _

该参数首先传递给 y，因此我们有

        y :: p -> _

之后，因为 y 也是 x

的第一个参数

        x :: (p -> _) -> _

此外，x 然后接受（在管道中）来自 y

的任何内容

        y :: p -> r
        x :: (p -> r) -> r -> _

我们把最后的结果称为q

        y :: p -> r
        x :: (p -> r) -> r -> q

并写出给定的整个函数：

(\x y -> x y . y) :: ((p -> r) -> r -> q) -> (p -> r) -> p -> q
--                   └─────────x────────┘    └──y───┘

也就是说，重命名类型变量后，与您开始时的名称相同。

Answer 2

根据f x y z = x y (y z)，你可以推理如下：

我们没有将 z 应用到任何东西，所以它可以有一些任意类型；称它为 u1（对于未知的第一名）。
y应用于z，所以它的参数类型是u1，但是return类型是另一个未知类型u2.因此 y :: u1 -> u2.
y z 因此类型为 u2.
x 应用于 y 和 y z，因此必须具有类似于 [=25] 的类型=];没有理由假设任一参数具有相同的类型，或者任一类型与 return 类型相同。
f的return值与x的return值相同，即u3。

总而言之，我们有

f :: ((u1 -> u2) -> u2 -> u3) -> (u1 -> u2) -> u1          ->    u3
     ------------------------    ----------    --                --
         type of x                type of y    type of z        end result of f

因为除了将不同的类型分开之外，各个类型变量的名称并不重要，我们可以使用

重命名它们

u1 ~ b
u2 ~ a
u3 ~ c

获取您查找的类型

f :: ((b  -> a) -> a  -> c) -> (b  -> a) -> b  -> c

haskell 函数类型简化 f :: ((b -> a ) -> a -> c ) -> (b -> a ) -> b -> c

haskell function type simplifyed f :: ((b -> a ) -> a -> c ) -> (b -> a ) -> b -> c

haskell

types

functional-programming

logic

declarative