haskell - 如何轻松应对Haskell上的类型系统？

Question

Haskell的类型系统功能强大，并因其数学上的严格性和逻辑上的合理性而广受赞誉，另一方面，如下所示的幼稚让我怀疑为什么它不按直觉预期起作用？

例如。为什么不能将Int转换为Num上的x3，但是f1接受签名Int的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 type system轻松处理类型系统，甚至找到一些不错的著作，例如1，2，3和4用于使其神秘化。如果您曾经遇到挑战并克服挑战，还想提出什么建议？

@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的超类型，当Num用x6注释类型时，它就是Num本身。但是，如果我们随后将Num从Int转换为(x6::Int)::Num a => a，则在x6的Num之后的Int的串联类型注释将无法统一。因此，
此处不满足Num的第一个推断类型x6。

Answer 1

为什么不能将Int转换为Num上的x3

Int无法转换为Num，因为Int是类型，而Num是类型类。这两种实体之间的区别有望在接下来的内容中变得清晰。

Int无法转换为其他任何东西，因为Haskell在您在此使用的意义上没有任何转换。没有隐式强制转换。确实发生的事情是多态类型专门化为某种确定类型。但是，确定类型永远不会自动变为其他类型。

考虑到这一点，让我们考虑一下您的示例。

Prelude> let x1 = 1
Prelude> :t x1
x1 :: Num a => a

x1在这里是多态的，这意味着它可以根据您的使用方式采用不同的类型。这种不确定性可以通过类型变量a的存在来识别(类型变量与具体类型不同，不大写)。 x1的类型尽管是多态的，但在某种程度上受约束Num a约束。 Num a => a可以理解为“具有类型Num类型实例的任何类型”，而普通的a则意味着“任何类型的任何东西”。

Prelude> let x2 = 1 :: Int
Prelude> :t x2
x2 :: Int

引入类型注释:: Int意味着请求Int与1的类型Num a => a统一。在这种情况下，这仅意味着将类型变量a替换为Int。鉴于Int确实有一个Num实例，这是一个有效的举动，类型检查器很乐意接受它。类型注释将1的多态类型专门化为Int。

Prelude> let x3 = (1 :: Int) :: Num a => a
Couldn't match expected type ‘a1’ with actual type ‘Int’

1 :: Int的类型是Int。第二个注释要求使用Num a => a对其进行统一。但是，那是不可能的。一旦指定了类型，就不能仅通过提供类型注释来“忘记”该类型并还原该专业化。也许您正在考虑OOP转换；这根本不是一回事。顺便说一句，如果类型检查器接受x3，那么您将能够编写x4 = ((1 :: Int) :: Num a => a) :: Double，从而将Int转换为Double。但是，在一般情况下，这种转换不可能像这样发生，因为您没有告诉我们如何进行转换。至于特殊情况，没有。 (将Int转换为Double当然是可能的，但是它需要适当的功能。例如，您可能会发现考虑fromIntegral的类型与其功能之间的关系是很重要的。)

Prelude> let f1 :: Num a => a -> a; f1 = id
Prelude> :t f1 (1 :: Int)
f1 (1 :: Int) :: Int

这里的原理保持不变。唯一的区别是您必须考虑参数和结果的类型如何相互关联。 id的类型是a -> a。它专门适合Num a => a -> a。传递Int参数进一步将其专用于Int -> Int，因此您得到的类型为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参数的函数。

Prelude> let f3 :: Num a => a -> Int; f3 = id
Couldn't match type ‘a’ with ‘Int’

在这里，您想用a -> a统一id的类型Num a => a -> Int。但是，如果将a替换为Double中的Num a => a -> Int，则会得到Double -> Int，它不可能与a -> a统一，因为它会更改类型，而a -> a不会更改。 (这就是Thomas M. DuBuisson在上面的评论的意思:您的实现类型与id不兼容，因为id不能更改任何类型。)

Prelude> let f4 :: Num a => Int -> a; f4 = id
Couldn't match type ‘a’ with ‘Int’

最后，这类似于f3，除了不匹配发生在结果类型上而不是参数的类型上。这次放一个不同的旋转，您无法通过使用Num a => Int -> a实例(例如Num，Int等)设置特定类型，然后将其“上载”到Double来实现Num a => a函数，因为没有这样的事相反，Num a => Int -> a必须适用于具有a实例的任何Num选择。