39

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

4

6 回答 6

24

具体来说，是什么造就了 Haskell 的类型系统

在过去的十年中，它被设计成既灵活——作为属性验证的逻辑——又强大。

Haskell 的类型系统多年来一直在发展，以鼓励相对灵活、富有表现力的静态检查学科，几组研究人员确定了能够实现强大的新类编译时验证的类型系统技术。Scala 在该领域相对不发达。

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

一些论文说明了 Haskell 类型系统的工程工作所采取的方向：

于 2010-09-24T15:30:48.133 回答
14

Hindley-Milner 不是类型系统，而是类型推断算法。在过去，Haskell 的类型系统曾经能够使用 HM 进行完全推断，但那艘船早已航行到带有扩展的现代 Haskell 上。（ML 仍然能够被完全推断）。

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

但这在很大程度上不是我认为问题的真正意义所在。

没有链接的论文指向另一个方面——Haskell 类型系统的扩展使其图灵完备（现代类型家族使图灵完备语言更接近于值级编程）。关于这个主题的另一篇不错的论文是 McBride 的Faking It: Simulating Dependent Types in Haskell。

关于 Scala 的另一个线程中的论文：“Type Classes as Objects and Implicits”深入探讨了为什么实际上您也可以在 Scala 中完成大部分操作，尽管更加明确。我倾向于感觉，但这更像是一种直觉，而不是真正的 Scala 体验，它更特别和明确的方法（C++ 讨论称为“名义”）最终有点混乱。

于 2010-09-24T15:53:56.140 回答
11

让我们来看一个非常简单的例子：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++ 类型 ofsumJusts没有指定它需要+并从0. 当事情不工作时出现的错误消息是神秘而奇怪的。在 Haskell 中，编译器只会抱怨类型不是 的实例Num，非常简单..

简而言之，Haskell 有：

  • ADT
  • 类型类
  • 一个非常友好的语法和对泛型的良好支持（在 C++ 中人们试图避免因为他们所有的神秘主义）
于 2010-09-27T19:50:09.553 回答
8

Haskell 语言允许您在不放弃功能的情况下编写更安全的代码。现在大多数语言都以安全为代价来交换特性：Haskell 语言的存在表明两者兼有是可能的。

我们可以在没有空指针、显式转换、松散类型的情况下生活，并且仍然拥有完美表达的语言，能够生成高效的最终代码。

此外，Haskell 类型系统以及其默认惰性和纯编码方法为您提供了复杂但重要的问题，如并行性和并发性。

只是我的两分钱。

于 2010-09-24T15:57:46.583 回答
6

在其他语言中我真正喜欢和怀念的一件事是对类型类的支持，这是对许多问题（包括例如多变量函数）的优雅解决方案。

使用类型类，定义非常抽象的函数非常容易，这些函数仍然是完全类型安全的——比如这个斐波那契函数：

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

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

于 2010-09-24T14:53:51.543 回答
0

什么是表现力？据我了解，类型系统允许我们对代码施加什么约束，或者换句话说，我们可以证明代码的哪些属性。类型系统的表现力越强，我们可以在类型级别嵌入的信息就越多（类型检查器可以在编译时使用这些信息来检查我们的代码）。
这里有一些其他语言没有的 Haskell 类型系统的特性。

  1. 纯度。
    Purity 允许 Haskell 区分纯代码和支持 IO 的代码
  2. 参数化。
    Haskell 强制参数化多态函数的参数化，因此它们必须遵守一些定律。（某些语言确实允许您表达多态函数类型，但它们不强制参数化，例如 Scala 允许您对特定类型进行模式匹配，即使参数是多态的）
  3. ADT
  4. 扩展
    Haskell 的基本类型系统是 λ2 的较弱版本，它本身并不令人印象深刻。但是有了这些扩展，它变得非常强大（甚至能够用单例表示依赖类型）：
    1. 存在类型
    2. rank-n 类型（全 λ2）
    3. 类型族
    4. 数据类型（允许在类型级别进行“类型化”编程）
    5. 加特...
于 2020-02-16T13:34:31.270 回答