是什么让Haskell的类型系统比其他语言的类型系统更"强大"？

Question

阅读Scala类型系统与Haskell的缺点？我不得不问:具体来说,它使Haskell的类型系统比其他语言的类型系统(C,C++,Java)更强大.显然,即使Scala也不能执行与Haskell类型系统相同的功能.具体来说,是什么让Haskell的类型系统(Hindley-Milner类型推断)如此强大？你能给我举个例子吗？

Answer 1

具体来说,它是什么使Haskell的类型系统

它在过去十年中被设计为灵活 - 作为财产验证的逻辑 - 并且功能强大.

多年来,Haskell的类型系统已经开发出来,以鼓励一种相对灵活,富有表现力的静态检查规则,由几组研究人员识别可以实现强大的新类型编译时验证的类型系统技术.Scala在该地区相对不发达.

也就是说,Haskell/GHC提供了一个强大的逻辑,旨在鼓励类型级编程.函数式编程世界中相当独特的东西.

一些文章介绍了Haskell类型系统的工程设计方向:

• 有趣的类型功能
• 与类相关的类型
• 功能依赖的乐趣

Answer 2

Hindley-Milner不是一个类型系统,而是一种类型推理算法.Haskell的类型系统,在当天,曾经可以使用HM完全推断,但是这艘船长期以来用于现代Haskell扩展.(ML仍然能够被完全推断).

可以说,主要或完全推断所有类型的能力在表达方面产生了力量.

但这在很大程度上不是我认为问题的真正含义.

dons链接的论文指向另一个方面 - Haskell类型系统的扩展使其完整(并且现代类型系列使得图灵完整语言更接近于价值级编程).关于这个主题的另一篇好文章是McBride的伪造:模拟Haskell中的依赖类型.

Scala中另一个帖子中的文章:"将类类型作为对象和隐含"进入了为什么你实际上可以在Scala中完成大部分工作,尽管有更多的显式性.我倾向于感觉到,但这更像是一种直觉而非真实的Scala体验,它更加特殊和明确的方法(C++讨论称之为"名义")最终有点混乱.

Answer 3

让我们来看一个非常简单的例子:Haskell Maybe.

data Maybe a = Nothing | Just a

在C++中:

template <T>
struct Maybe {
    bool isJust;
    T value;  // IMPORTANT: must ignore when !isJust
};

让我们在Haskell中考虑这两个函数签名:

sumJusts :: Num a => [Maybe a] -> a

和C++:

template <T> T sumJusts(vector<maybe<T> >);

区别:

• 在C++中,可能存在更多错误.编译器不检查使用规则Maybe.
• C++类型sumJusts没有指定它需要+和强制转换0.当事情不起作用时出现的错误信息是神秘而奇怪的.在Haskell中,编译器会抱怨该类型不是一个实例Num,非常简单.

简而言之,Haskell有:

• 抽象数据类型
• 型类
• 一个非常友好的语法和对泛型的良好支持(在C++中人们试图避免因为他们所有的密码学原因)

Answer 4

Haskell语言允许您编写更安全的代码而不会放弃功能.现在大多数语言都是为了安全而交换功能:Haskell语言可以显示两种语言都有可能.

我们可以在没有空指针,显式演员,松散打字的情况下生活,并且仍然具有完美的表达语言,能够生成有效的最终代码.

更重要的是,Haskell类型系统,以及它的默认和纯粹的编码方法,可以提高复杂性,但是并行性和并发性等重要问题.

只是我的两分钱.

Answer 5

我非常喜欢和错过其他语言的一件事是支持类型,这是许多问题(包括例如多变量函数)的优雅解决方案.

使用类型类,定义非常抽象的函数非常容易,这些函数仍然是完全类型安全的 - 比如这个Fibonacci函数:

fibs :: Num a => [a]
fibs@(_:xs) = 0:1:zipWith (+) fibs xs

例如:

map (`div` 2) fibs        -- integral context
(fibs !! 10) + 1.234      -- rational context
map (:+ 1.0) fibs         -- Complex  context

您甚至可以为此定义自己的数字类型.