如何在Haskell上轻松处理类型系统？ [英] How to comfortably deal with the type system on Haskell?

问题描述

Haskell的类型系统非常强大，并且喜欢它的数学严格性和逻辑性，另一方面，像以下那样幼稚的东西让我想知道为什么它不像直觉那样工作？

例如，为什么不能在 x3 上将 Int 转换为 Num 但 f1 接受 Int 对签名 Num ？

  Prelude>让x1 = 1 
 Prelude> ：t x1 
 x1 :: Num a => a 
 
前奏>让x2 = 1 :: Int 
 Prelude> ：t x2 
 x2 :: Int 
 
 Prelude>让x3 =（1 :: Int）:: Num a => a 
无法与实际类型'Int'匹配的预期类型'a1'
 
前奏>让f1 :: Num a => a  - >一个; f1 = id 
前奏> ：t f1（1 :: Int）
 f1（1 :: Int）:: Int 
 
 Prelude>让f2 :: Int  - >诠释; f2 = id 
前奏> ：t f2 1 
 f2 1 :: Int 
 
 Prelude>让f3 :: Num a => a  - >诠释; f3 = id 
 
前奏>让f4 :: Num a => Int  - >一个; f4 = id 
无法将类型'a'与'Int'匹配
  

我知道人们应该最终学习基础理论，例如 HM类型系统以舒适地处理类型系统，甚至找到一些漂亮的作品，例如 1 ， 2 ， 3 和 4 。

@EDIT
$您还有什么建议可以推荐？ b $ b

  Prelude>让f5 x5 = x5 :: Int 
 Prelude> ：t f5 
 f5 :: Int  - > Int 
 
前奏>让f6 x6 = x6 :: Num a => a 
无法与实际类型为't'的预期类型'a1'匹配
  

第一， x6 必须是 Num 的超类型，即 Num 本身，当 x6 类型注释为 Num 时。但是，（x6 :: Int）的 Int 之后的 Num 的连接类型注释： ：Num a =>如果我们将 x6 从 Num 降到<$ c，那么 $ C>内部。因此，这里不满足
x6 的第一个推断类型 Num 。

$ b $为什么不能将 Int 转换为<$ c $ c> Num x3

1. Int 不能转换为 Num ，因为 Int 是一个类型， Num 是一个类型的类。这两种实体之间的区别有望在下面变得清楚。

2. Int 转换为其他任何东西，因为Haskell在这里使用的意义上没有转换。没有隐式转换。发生什么事情是一种多态类型，使某些特定类型的专用;然而，一个明确的类型永远不会自动成为别的东西。

，让我们来看看你的例子。

  Prelude>让x1 = 1 
 Prelude> ：t x1 
 x1 :: Num a => a 
  

x1 这里是 polymorphic ，这意味着它可以采取不同的类型，具体取决于你如何使用它。这种不确定性可以通过类型变量 a 的存在来识别（类型变量，与具体类型不同，不会大写）。 x1 的类型虽然是多态的，但在某种程度上受约束限制 Num a 。 Num a =>一个可以被解读为任何类型的类型为类型的类 Num ，而普通的 a 意味着任何类型。

  Prelude>让x2 = 1 :: Int 
 Prelude> ：t x2 
 x2 :: Int 
  

引入类型注释 :: Int 意味着请求 Int 与< 1 c $ c>， Num a =>一个。在这种情况下，这仅仅意味着用 Int 替换类型变量 a 。鉴于 Int 确实有一个 Num 的实例，这是一个有效的举动，类型检查器很高兴地接受它。类型注释专注于 1 到 Int 。

的多态类型。

  Prelude>让x3 =（1 :: Int）:: Num a => a 
无法与实际类型'Int'匹配的预期类型'a1'
  

类型 1 :: Int 是 Int 。第二个注释要求将它与 Num a =>一个。然而，这是不可能的。一旦一个类型被专门化，你就不能忘记这个类型，只需提供一个类型注释就可以恢复专业化。也许你正在考虑OOP上传;这不完全相同。顺便说一下，如果类型检查器接受 x3 ，那么您可以编写 x4 =（（（1 :: Int）:: Num a = > a）:: Double ，从而将 Int 转换为 Double 。但是，在一般情况下，这种转换不可能像这样发生，因为您没有告诉转换是如何完成的;至于特例，则没有。 （将 Int 转换为 Double 当然是可能的，但它需要一个适当的函数。例如，你可能会发现它应该考虑来自整合的类型与它的作用有何关系。）

 前奏>让f1 :: Num a => a  - >一个; f1 = id 
前奏> ：t f1（1 :: Int）
 f1（1 :: Int）:: Int 
  



<这里的原则保持不变。唯一的区别是你必须考虑论证和结果的类型是如何相互关联的。 id 的类型是 a - >一个。它专精于 Num a => a - >一个。传递 Int 参数进一步将它专门化为 Int - > Int ，所以你得到类型为 Int 的结果。



 前奏>让f2 :: Int  - >诠释; f2 = id 
前奏> ：t f2 1 
 f2 1 :: Int 
  

f1 有一个多态类型，通过给它提供一个 Int 参数来专门化，而 f2 有一个单形类型，所以不需要专门化。 id 是专门从 a - >一个直接指向 Int - > Int ，而 1 是专门从 Num a => a 到 Int ，因为您正在将它提供给需要 Int 参数的函数。

  Prelude>让f3 :: Num a => a  - >诠释; f3 = id 
无法将类型'a'与'Int'匹配
  

你想统一 a - >一个， id 的类型，其中 Num a => a - > INT 。但是，如果用中的 Double 替换 a > Num a => a - > Int ，你得到 Double - > Int ，它不可能与 a - > a ，因为它会改变类型，而 a - >一个不会。 （这是Thomas M. DuBuisson上面评论的观点：你的实现类型与 id 不兼容，因为 id

  Prelude>让f4 :: Num a => Int  - >一个; f4 = id 
无法将类型'a'与'Int'匹配
  

这与 f3 类似，只是不匹配发生在结果类型上而不是参数上。这次放置一个不同的旋转，你不能实现 Num a => Int - >使用 Num 实例（无论是 Int ）来解决特定类型的函数， Double 等），然后上传到 Num a =>一个，因为没有这样的事情上传。相反 Num a => Int - >一个必须适用于 a 任何 c $ c> num code>。

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?

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’

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’

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.

解决方案

why can't Int be converted to Num on x3

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.

2. 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 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

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’

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

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 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’

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’

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屋！