下面的等式是用Miranda语法编写的,但由于Miranda和Haskell之间的相似性,我希望Haskell程序员应该理解它!
如果定义以下功能:
rc v g i = g (v:i)
rn x = x
rh g = hd (g [])
f [] y = y
f (x:xs) y = f xs (rc x y)
g [] y = y
g (x:xs) y = g xs (x:y)
你如何计算出函数的类型？我想我理解如何为f,g和rn解决这个问题,但我对部分应用程序部分感到困惑.
将是* - >*(或任何东西 - >任何东西,我认为它是 - > Haskell中的一个？)
对于f和g,函数类型是[*] - >* - >*？
我不确定如何找到rc和rh的类型.在rc中,g被部分地应用于变量i - 所以我猜这会将i的类型约束为[*].rc和g在rc的定义中应用了什么顺序？是否将g应用于i,然后将结果函数用作rc的参数？或者rc是否采用v,g和i的3个独立参数？我真的很困惑..任何帮助将不胜感激!多谢你们.
抱歉忘了添加hd是列表的标准head函数,定义如下:
hd :: [*] -> *
hd (a:x) = a
hd [] = error "hd []"
该类型是从已知的类型以及定义中如何使用表达式推断出来的.
让我们从顶部开始,
rc v g i = g (v : i)
所以rc :: a -> b -> c -> d,我们必须看到可以找到什么a, b, c和d.在右侧,出现了(v : i),所以v :: a我们看到了i :: [a],c = [a].然后g被施加到v : i,因此g :: [a] -> d,总共,
rc :: a -> ([a] -> d) -> [a] -> d
rn x = x意味着对参数类型没有约束,rn并且它的返回类型是相同的,rn :: a -> a.
rh g = hd (g [])
由于rh's参数g应用于RHS上的空列表,因此它必须具有类型[a] -> b,可能有更多关于a或b遵循的信息.事实上,g []是的说法hd在RHS,那么g [] :: [c]和g :: [a] -> [c],由此
rh :: ([a] -> [c]) -> c
下一个
f [] y = y
f (x:xs) y = f xs (rc x y)
第一个参数是一个列表,如果是空的,结果是第二个参数,所以f :: [a] -> b -> b从第一个方程开始.现在,在第二个等式中,在RHS上,第二个参数f是rc x y,因此rc x y必须具有相同的类型y,我们称之为b.但
rc :: a -> ([a] -> d) -> [a] -> d
所以b = [a] -> d.于是
f :: [a] -> ([a] -> d) -> [a] -> d
最后
g [] y = y
g (x:xs) y = g xs (x:y)
从我们推导出的第一个方程式开始g :: [a] -> b -> b.从第二个开始,我们推断出b = [a],因为我们采取了g第一个论点的头,因此将其限制在第二个论点
g :: [a] -> [a] -> [a]
我将使用haskell语法来编写类型.
rc v g i = g (v:i)
这里rc有三个参数,所以它的类型会是这样的a -> b -> c -> d.
v:i必须是与v和相同类型的元素列表i,所以v :: a和i :: [a].
g应用于该列表,以便g :: [a] -> d.如果你把所有这些放在一起,你得到rc :: a -> ([a] -> d) -> [a] -> d.
正如你已经想到的那样rn :: a -> a,因为它只是身份.
我不知道hd你使用的函数的类型rh,所以我会跳过它.
f [] y = y
f (x:xs) y = f xs (rc x y)
这里f有两个参数,所以它的类型就像a -> b -> c.从第一种情况我们可以推断出b == c,因为我们返回y,并且第一个参数是一个列表.现在我们知道了f :: [a'] -> b -> b.在第二种情况下,请注意输入中的输入x和y输出rc:y必须是一个函数[a'] -> d,并且rc x y :: a' -> d(必须也是类型y,因为它是作为第二个参数传递的f).最后,我们可以这么说f :: [a'] -> ([a'] -> d) -> ([a'] -> d).由于->是右关联,这相当于[a'] -> ([a'] -> d) -> [a'] -> d.
您可以以相同的方式推断其余的.