如何在Haskell上轻松处理类型系统？

Question

Haskell的类型系统功能强大,并且因其数学严谨性和逻辑性而受到欢迎,另一方面,如下所述的天真使我想知道为什么它不能像直觉那样工作？

例如,为什么不能Int转换为Numon 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型系统到舒适与类型系统处理,甚至还发现了一些不错的作品,例如1,2,3和4的神秘化了.如果你遇到过这个挑战,你还想推荐什么呢？

@编辑

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必须是超类型.然而,串连式注解后的不团结,如果我们再垂头丧气的到.因此,第一推断类型的不满意这里.NumNumx6NumNumInt(x6::Int)::Num a => ax6NumIntNumx6

Answer 1

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

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

2. 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,从而将Inta 转换为a Double.但是,在一般情况下,这种转换无法像这样发生,因为您没有告诉转换是如何完成的; 至于特殊情况,没有任何.(将Inta 转换为a 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.