如何确定q2和q3的类型?当我输入时,模块给了我类型,但是手动执行此操作的可靠方法是什么?请帮忙.谢谢.
q2 x y z w = w (x y) (z y)
Type is: q2 :: (a -> b) -> a -> (a -> c) -> (b -> c -> d) -> d
q3 f g x y = (f.g) x == y
Type is: q3 :: Eq a => (b -> a) -> (c -> b) -> c -> a -> Bool
Run Code Online (Sandbox Code Playgroud)
J. *_*son 11
输入信息从现有结构流向新结构.我们来看看你的例子:
q2 x y z w = w (x y) (z y)
Run Code Online (Sandbox Code Playgroud)
它可能并不明显,但是这个函数已经调用了一些类型化的Haskell原语.特别是,它使用具有类型的函数应用程序
($) :: (a -> b) -> a -> b
Run Code Online (Sandbox Code Playgroud)
事实上,我们可以使用这样的($)语法来使我们对函数应用程序的使用更加明确.
q2 x y z w = (w $ x $ y) $ z $ y
Run Code Online (Sandbox Code Playgroud)
或者,我们可以用Javascript-esque语法重新构造它,以便再次更清楚地看到应用程序
q2(x)(y)(z)(w) = w(x(y))(z(y))
Run Code Online (Sandbox Code Playgroud)
无论如何,应该清楚的是,有4个功能应用程序正在发生.从这些我们将产生给我们主要类型的信息q2.
扩展类型推断的主要方法是"统一",也就是说,如果我们知道单个事物具有类型A,B那么我们必须能够转换A并B进入C,第三种类型同时兼顾A和B.它可能只是A或者B甚至是.
| A | B | C |
|--------|--------|--------|
| String | a | String |
| Int | String | <fail> |
| a | b | c | (where we suppose a == b == c)
| a -> b | c -> d | e -> f | (where we suppose a == c == e
| | | | and b == d == f)
Run Code Online (Sandbox Code Playgroud)
正如您所看到的,统一的另外两个特征:(1)它可能会失败,如果和(2)它有时会导致我们假设类型变量之间的平等.
一般来说,这就是推理的进展:我们为所有我们不知道的事物分配一个新的类型变量,然后尝试统一所有的部分.一路上我们可能会失败(因此我们说类型检查已经失败)或者我们将收集一大堆相等性,这些等式告诉我们已经引入了许多冗余类型变量.然后我们通过消除所有冗余变量来总结信息,直到我们不再需要陈述我们的等式.
id :: a -> a
3 :: Num a => a
3 :: Num b => b -- make the variable fresh / not conflict with `a`
id 3 :: Num c => c (supposing a == b == c)
id 3 :: Num a => a (supposing nothing, we've forgotten about b and c)
Run Code Online (Sandbox Code Playgroud)
所以我们可以应用这个过程q2.算术上做起来有点啰嗦,但很容易手工完成.我们正在寻找价值的类型q2.我们知道q2需要4个参数并返回一些东西,所以我们可以立即构建该类型
q2 :: a -> b -> c -> d -> e
Run Code Online (Sandbox Code Playgroud)
我们知道,通过统一的类型x,z以及w与应用程序的类型($),该类型a和c必须与功能兼容
q2 :: (f -> g) -> b -> (h -> i) -> d -> e
Run Code Online (Sandbox Code Playgroud)
并且他们的输入参数必须具有与其参数值兼容的类型 y :: b
q2 :: (b -> g) -> b -> (b -> i) -> d -> e
Run Code Online (Sandbox Code Playgroud)
最后我们可以检查w它是一个函数,它接受一个类型的参数x y并返回另一个函数,它接受一个类型的参数z y并返回一些东西
q2 :: (b -> g) -> b -> (b -> i) -> (g -> (i -> j)) -> e
Run Code Online (Sandbox Code Playgroud)
由(->)我们通常写的右相关性
q2 :: (b -> g) -> b -> (b -> i) -> (g -> i -> j) -> e
Run Code Online (Sandbox Code Playgroud)
最后,我们知道返回类型w是整个函数的返回类型
q2 :: (b -> g) -> b -> (b -> i) -> (g -> i -> j) -> j
Run Code Online (Sandbox Code Playgroud)
其中,直到重命名,是最终的,最常见的类型q2.
欲了解更多信息,调查辛德米尔纳和算法W¯¯.我已经松散地涵盖了大部分细节,但还有一些剩余的想法,所有这些都可以更仔细地检查.
那就是分析有意义的事情:
首先我们有
q2 x y z w = w (x y) (z y)
Run Code Online (Sandbox Code Playgroud)
让我们分解它,从q2 x y z w我们看到它需要4个参数,以及返回类型:
q2 :: a -> b -> c -> d -> e
Run Code Online (Sandbox Code Playgroud)
现在我们看一下这些,我们有w (x y) (z y),让我们分成小块:
(x y):我们使用x函数作为函数y的参数,因此x有一个类型x :: b -> f.所以q2现在看起来像这样:
q2 :: (b -> f) -> b -> c -> d -> e
Run Code Online (Sandbox Code Playgroud)(z y):具有相同的风格,所以我们可以说,我们对所说的一样x,但我们不知道是否x和z返还相同种类,所以z应该是这样的z :: b -> g.使q2这个样子的:
q2 :: (b -> f) -> b -> (b -> g) -> d -> e
Run Code Online (Sandbox Code Playgroud)
注意: (b -> f)并(b -> g)返回不同的类型,因为没有迹象(至少到现在为止)它们返回相同的类型.
w (x y) (z y):这里我们使用w的功能,同时作为参数(x y)和(z y),所以现在w有一个类型w :: f -> g -> h.制作q2:
q2 :: (b -> f) -> b -> (b -> g) -> (f -> g -> h) -> e
Run Code Online (Sandbox Code Playgroud)
注: w需要的返回类型的参数x和z.
q2 x y z w = w (x y) (z y):我们可以看到这个函数做的最后一件事是w用作函数,所以w返回的是q2应该返回的内容,所以最后q2看起来像这样:
q2 :: (b -> f) -> b -> (b -> g) -> (f -> g -> h) -> h
Run Code Online (Sandbox Code Playgroud)希望它有所帮助,你应该q3自己动手练习.如果您遇到困难,请告诉我.