如何轻松应对 Haskell 上的类型系统? [英] How to comfortably deal with the type system on Haskell?
问题描述
Haskell 的类型系统功能强大,因其数学严谨性和逻辑合理性而广受喜爱,另一方面,像下面这样幼稚的东西让我想知道为什么它不能按直觉预期工作?
Haskell's type system is powerful and liked for its mathematical rigorousness and logical soundness, on the other side something as naive as below makes me wonder why it doesn't work as expected by intuition?
例如为什么 Int
不能在 x3
上转换为 Num
但 f1
接受 Int
反对签名Num
?
E.g. why can't Int
be converted to Num
on x3
but f1
accept Int
against the signature Num
?
Prelude> let x1 = 1
Prelude> :t x1
x1 :: Num a => a
Prelude> let x2 = 1 :: Int
Prelude> :t x2
x2 :: Int
Prelude> let x3 = (1 :: Int) :: Num a => a
Couldn't match expected type ‘a1’ with actual type ‘Int’
Prelude> let f1 :: Num a => a -> a; f1 = id
Prelude> :t f1 (1 :: Int)
f1 (1 :: Int) :: Int
Prelude> let f2 :: Int -> Int; f2 = id
Prelude> :t f2 1
f2 1 :: Int
Prelude> let f3 :: Num a => a -> Int; f3 = id
Prelude> let f4 :: Num a => Int -> a; f4 = id
Couldn't match type ‘a’ with ‘Int’
我知道人们最终应该学习基础理论,例如HM 类型系统 轻松应对类型系统,甚至发现一些不错的作品,例如1, 2, 3 和 4 揭开它的神秘面纱.如果您曾经遇到过并克服了这一挑战,您还想推荐什么?
I knew that one should finally learn the underlying theory e.g. HM type system to comfortably deal with the type system, and even found some nice writings e.g. 1, 2, 3 and 4 for demystifying it. What else would you like to recommend if you ever came cross and overcame this challenge?
@EDIT
Prelude> let f5 x5 = x5::Int
Prelude> :t f5
f5 :: Int -> Int
Prelude> let f6 x6 = x6::Num a => a
Couldn't match expected type ‘a1’ with actual type ‘t’
首先,x6
必须是 Num
的超类型,当 x6
被类型注释时,它本身就是 Num
与 Num
.但是,(x6::Int)::Num a => 的
将不会合并.因此,Int
之后的 Num
的连接类型注释.如果我们随后将 x6
从 Num
向下转换为 Int
,则 ax6
的第一个推断类型 Num
在这里不满足.
First, x6
must have been a supertype of Num
that is Num
itself when x6
is type annotated with Num
. However, the concatenate type annotations for Num
after Int
of (x6::Int)::Num a => a
won't be united if we then downcast x6
from Num
to Int
. Hence,
the first inferred type Num
of x6
is unsatisfied here.
推荐答案
为什么
Int
不能在x3
Int
无法转换为Num
因为Int
是一个类型,而Num
是一个 类型类.这两种实体之间的区别有望在下文中变得清晰.
Int
cannot be converted toNum
becauseInt
is a type andNum
is a type class. The difference between these two kinds of entities will hopefully become clear in what follows.
Int
无法转换为其他任何东西,因为 Haskell 没有您在此处使用的意义上的转换.没有隐式强制转换.确实发生的是多态类型将专门化 到某种确定的类型;然而,一个确定的类型永远不会自动变成别的东西.
Int
cannot be converted to anything else because Haskell has no conversions in the sense you are using here. There are no implicit casts. What does happen is a polymorphic type getting specialised to some definite type; however, a definite type never becomes something else automatically.
考虑到这一点,让我们考虑一下您的示例.
With that in mind, let's consider your examples.
Prelude> let x1 = 1
Prelude> :t x1
x1 :: Num a => a
x1
这里是多态,这意味着它可以根据你的使用方式假设不同的类型.这种不确定性可以通过类型变量 a
的存在来识别(类型变量与具体类型不同,不是大写的).x1
的类型虽然是多态的,但在一定程度上受到约束 Num a
的限制.Num a =>;a
可以理解为具有 type class Num
实例的任何类型",而普通的 a
则意味着任何类型".
x1
here is polymorphic, which means it can assume different types depending on how you use it. This indeterminacy can be recognised by the presence of the type variable a
(type variables, unlike concrete types, are not capitalised). The type of x1
, though polymorphic, is to some extent restricted by the constraint Num a
. Num a => a
can be read as "any type that has an instance of the type class Num
", while a plain a
would mean "any type whatsoever".
Prelude> let x2 = 1 :: Int
Prelude> :t x2
x2 :: Int
引入类型注解::Int
表示要求Int
与1
的类型统一,Num a =>;一个代码>.在这种情况下,这仅仅意味着将类型变量
a
替换为 Int
.鉴于 Int
确实有一个 Num
的实例,这是一个有效的移动,并且类型检查器很乐意接受它.类型注解专门将1
的多态类型转为Int
.
Introducing the type annotation :: Int
means requesting Int
to be unified with the type of 1
, Num a => a
. In this case, that simply means replacing the type variable a
with Int
. Given that Int
does have an instance of Num
, that is a valid move, and the type checker happily accepts it. The type annotation specialises the polymorphic type of 1
to Int
.
Prelude> let x3 = (1 :: Int) :: Num a => a
Couldn't match expected type ‘a1’ with actual type ‘Int’
1 :: Int
的类型是 Int
.第二个注释要求将其与 Num a =>; 统一起来.一个代码>.然而,这是不可能的.一旦一个类型被特化,你就不能仅仅通过提供类型注释来忘记"该类型并恢复特化.也许您正在考虑 OOP 向上转型;这根本不是一回事.顺便说一句,如果类型检查器接受
x3
,您将能够编写 x4 = ((1 :: Int) :: Num a => a) :: Double
,从而将 Int
转换为 Double
.但是,在一般情况下,这种转换不可能像那样发生,因为您没有告诉 如何 进行转换;至于特殊情况,没有.(将 Int
转换为 Double
当然是可能的,但它需要适当的函数.例如,您可能会发现考虑 fromIntegral 的类型如何
与它的作用有关.)
The type of 1 :: Int
is Int
. The second annotation demands unifying it with Num a => a
. That, however, is impossible. Once a type is specialised, you can't "forget" the type and revert the specialisation just by providing a type annotation. Perhaps you are thinking of OOP upcasting; this is not at all the same thing. By the way, if the type checker accepted x3
, you would be able to write x4 = ((1 :: Int) :: Num a => a) :: Double
, thus converting an Int
to a Double
. In the general case, though, there is no way this conversion can happen like that, as you didn't tell how the conversion is to be done; as for the special cases, there aren't any. (Converting an Int
to a Double
is certainly possible, but it requires an appropriate function. For instance, you may find it relevant to consider how the type of fromIntegral
relates to what it does.)
Prelude> let f1 :: Num a => a -> a; f1 = id
Prelude> :t f1 (1 :: Int)
f1 (1 :: Int) :: Int
这里的原则保持不变.唯一的区别是你必须考虑参数和结果的类型是如何相互关联的.id
的类型是 a ->;一个代码>.它专门用于
Num a =>一个->一个代码>.传递一个
Int
参数进一步将其专门化为 Int ->Int
,因此您会得到 Int
类型的结果.
The principles here remain the same. The only difference is that you have to consider how the types of argument and result are related to each other. The type of id
is a -> a
. It specialises just fine to Num a => a -> a
. Passing an Int
argument further specialises it to Int -> Int
, and so you get a result of type Int
.
Prelude> let f2 :: Int -> Int; f2 = id
Prelude> :t f2 1
f2 1 :: Int
f1
有一个多态类型,你可以通过给它一个 Int
参数来对其进行专门化,而 f2
有一个单态类型,所以有不需要专门化它.id
是专门从 a ->;a
直接到 Int ->Int
,而 1
特化自 Num a =>;a
到 Int
因为您将它提供给需要 Int
参数的函数.
f1
had a polymorphic type that you specialised by feeding it an Int
argument, while f2
has a monomorphic type, and so there is no need to specialise it. id
is specialised from a -> a
directly to Int -> Int
, while 1
is specialised from Num a => a
to Int
because you are feeding it to a function that expects an Int
argument.
Prelude> let f3 :: Num a => a -> Int; f3 = id
Couldn't match type ‘a’ with ‘Int’
这里,你要统一 a ->a
,id
的类型,Num a =>;一个->诠释
.但是,如果您将 a
替换为,例如 Num a => 中的
,你得到 Double
一个->IntDouble ->int
,不可能与 a -> 统一.a
,因为它在 a -> 时改变了类型一个
没有.(这就是 Thomas M. DuBuisson 上面评论的重点:您的实现类型与 id
的类型不兼容,因为 id
不能改变任何东西的类型.)
Here, you want to unify a -> a
, the type of id
, with Num a => a -> Int
. However, if you replace a
with, for instance, Double
in Num a => a -> Int
, you get Double -> Int
, which can't possibly unify with a -> a
, because it changes types while a -> a
doesn't. (That is the point of Thomas M. DuBuisson's comment above: the type of your implementations is not compatible with that of id
, because id
can't change the type of anything.)
Prelude> let f4 :: Num a => Int -> a; f4 = id
Couldn't match type ‘a’ with ‘Int’
最后,这就像 f3
一样,只是不匹配发生在结果类型而不是参数的类型上.这次换个角度,你不能实现 Num a =>诠释->a
函数,通过使用 Num
实例(可能是 Int
、Double
等)确定特定类型,然后 "将其向上转换为 Num a =>一个
,因为没有向上转换这样的东西.而是 Num a =>;诠释->a
必须适用于 任何 选择 a
的任何具有 Num
实例的选项.
Finally, this is just like f3
, except that the mismatch happens on the result type rather than on that of the argument. Putting a different spin on it this time, you can't implement a Num a => Int -> a
function by settling on a specific type with a Num
instance (be it Int
, Double
, etc.) and then "upcasting" it to Num a => a
, because there is no such thing as upcasting. Rather Num a => Int -> a
must work for any choice of a
whatsoever that has an instance of Num
.
这篇关于如何轻松应对 Haskell 上的类型系统?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!