从函数定义Haskell中推断函数类型

Question

所以我正在对Haskell进行测试,一个问题说:

让功能成为

lolo g x = ys
      where ys = [x] ++ filter (curry g x) ys

然后确定名为lolo的函数的类型.选项是:

a) (a,b) -> Bool -> b -> [(a,b)]
b) (b -> b -> b) -> Bool -> [b]
c) ((b,b) -> Bool) -> b -> [b]
d) (a -> b -> Bool) -> b -> [c]

有人可以解释它是哪一个,为什么？我真的很困惑这个......我不明白的是:

1)咖喱功能只适用于功能吗？不是可能是元组的数据类型？那么你可以推断出g在这种情况下是一个函数吗？如果g和x都是函数怎么办？是否有可能使用咖喱与第n个参数？我只看到咖喱与1参数一起使用.

2)我不太了解的另一件事是ys定义中的递归.所以ys是由ys定义的,但是在这种情况下我没有看到基本情况.它会永远结束吗？也许是过滤函数使递归结束.

3)还在咖喱gx =咖喱(gx)对吧？(这是关于功能应用优先级的问题)

非常感谢

Answer 1

1)curry必须是函数的第一个参数,它是所谓的高阶函数,它接受一个函数并返回一个新函数.虽然它的类型在GHCi中打印出来

curry :: ((a, b) -> c) -> a -> b -> c

它更明确地代表(IMO)

curry :: ((a, b) -> c) -> (a -> b -> c)

这使得它更明显地需要一个函数并返回一个新函数.从技术上讲,你可以说它curry有3个参数,一个是类型(a, b) -> c,一个是类型a,一个是类型b.它只需要一个通常接受参数元组并将其转换为带有2个参数的函数的函数.

2)计算ys永远不会结束,不要试图调用length它,你只需要永远运行计算.这不是问题,但是,您可以使用无限列表和非终止列表(非终止是一个列表,其中永远需要计算下一个元素,而不仅仅是具有无限元素的元素).但是,您仍然可以使用take和之类似的功能drop.

3)curry g x == curry (g x)吗？没有!当你看到这样的表达a b c d e,所有的b,c,d,和e是参数a.如果您改为查看a b c (d e),则e应用于d,并将结果应用于a b c.考虑一下filter even [1..10],这肯定不一样filter (even [1..10]),因为它甚至不会编译!(even :: Integral a => a -> Bool).

在解决此类问题时,首先要查看表达式中使用的函数,您已经知道了以下类型:

(++)   :: [a] -> [a] -> [a]
filter :: (b -> Bool) -> [b] -> [b]
curry  :: ((c, d) -> e) -> c -> d -> e

我在每个变量中都使用了不同的类型变量,这样在尝试排列类型时就会减少混淆.你可以通过加载GHCi然后输入来获得这些类型

> :type (++)
(++) :: [a] -> [a] -> [a]
> -- Or just use :t
> :t filter
filter :: (a -> Bool) -> [a] -> [a]
> :t curry
curry :: ((a, b) -> c) -> a -> b -> c

正如你所看到的,我已经改变了filter使用b的,而不是a和curry使用c,d以及e.这不会改变任何意义大于f x = x + 1对f y = y + 1,它只会使其更容易谈.

现在我们已经将功能分解为子组件,我们可以从"顶层"向下工作.顶部,我的意思是最后一个被调用的函数,即(++).您可以通过树像这样的功能

    (++)
   /    \
[x]     filter
       /      \
    curry     ys
   /     \
  g       x

所以我们可以清楚地看到它(++)位于顶部.使用它,我们可以推断出[x]具有类型[a],这意味着x ~ a(波浪号是类型相等符号),因此ys ~ [a],因此ys = [x] ++ something.现在我们知道了类型x,我们可以开始填写表达式的其余部分.接下来,我们努力工作filter (curry g x) ys.由于它是第二个参数(++),我们可以推断出这个子表达式也有类型[a].如果我们看一下类型filter:

filter :: (b -> Bool) -> [b] -> [b]

最终结果是类型列表[b].因为它被应用[x] ++,我们可以推断出来filter (curry g x) ys :: [a].这意味着[b] ~ [a] => b ~ a.作为参考,这是filter类型

filter :: (a -> Bool) -> [a] -> [a]

现在这个约束curry g x,它必须适合filter具有该类型的第一个参数a -> Bool.curry再看一下这个类型:

curry :: ((c, d) -> e) -> c -> d -> e

这意味着e ~ Bool,和d ~ a.如果我们重新插入它们

curry :: ((c, a) -> Bool) -> c -> a -> Bool

暂时忽略g,我们看看x我们想出的类型a.因为x是第二个参数curry,这意味着x匹配类型的参数c,暗示c ~ a.将其替换为我们刚刚计算出来的东西

curry :: ((a, a) -> Bool) -> a -> a -> Bool

同

               curry g x     :: a -> Bool
       filter (curry g x)    :: [a] -> [a]
       filter (curry g x) ys :: [a]
[x] ++ filter (curry g x) ys :: [a]

由此我们可以直接推断出lolo类型签名的结尾[a],所以

lolo :: ??? -> [a]

我会让你做剩下的几步来弄清楚是什么???.