如何轻松应对 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，则 a 将不会合并.因此，x6 的第一个推断类型 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

1. Int 无法转换为 Num 因为 Int 是一个类型，而 Num 是一个 类型类.这两种实体之间的区别有望在下文中变得清晰.

1. Int cannot be converted to Num because Int is a type and Num 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一个->Int，你得到 Double ->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屋！