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

发布于 2024-09-24 15:43:25 字数 312 浏览 8 评论 0原文

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

原文

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

霊感 2024-10-01 15:43:25

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

在过去十年中被设计得既灵活（作为属性验证的逻辑）又强大。

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

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

一些论文介绍了 Haskell 类型系统的工程工作的方向：

回复收藏 0 原文

一页 2024-10-01 15:43:25

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

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

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

没有链接的论文指出了另一个方面——Haskell 类型系统的扩展使其成为图灵完备的（并且现代类型系列使图灵完备的语言更加类似于值级编程）。关于这个主题的另一篇好论文是 McBride 的 Faking It: Simulated Dependent Types in哈斯克尔。

关于 Scala 的另一个线程中的论文：“将类作为对象和隐式”探讨了为什么实际上也可以在 Scala 中完成大部分工作，尽管更加明确。我倾向于感觉，但这更多的是一种直觉，而不是来自真正的 Scala 经验，它更临时和更明确的方法（C++ 讨论中所谓的“名义”）最终有点混乱。

回复收藏 0 原文

千秋岁 2024-10-01 15:43:25

让我们看一个非常简单的例子：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的使用规则。
sumJusts 的 C++ 类型未指定它需要 + 并从 0 进行转换。当事情不起作用时显示的错误消息是神秘且奇怪的。在 Haskell 中，编译器只会抱怨该类型不是 Num 的实例，非常简单。

简而言之，Haskell 具有：

ADT
类型类
非常友好的语法和对泛型的良好支持（这在C++ 人们试图避免，因为他们所有的神秘主义）

Let's go with a very simple example: Haskell's Maybe.

data Maybe a = Nothing | Just a

In C++:

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

Let's consider these two function signatures, in Haskell:

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

and C++:

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

Differences:

In C++ there are more possible mistakes to make. The compiler doesn't check the usage rule of Maybe.
The C++ type of sumJusts does not specify that it requires + and cast from 0. The error messages that show up when things do not work are cryptic and odd. In Haskell the compiler will just complain that the type is not an instance of Num, very straightforward..

In short, Haskell has:

ADTs
Type-classes
A very friendly syntax and good support for generics (which in C++ people try to avoid because of all their cryptickynessishisms)

回复收藏 0 原文

夏末 2024-10-01 15:43:25

Haskell 语言允许您编写更安全的代码，而无需放弃功能。如今，大多数语言都以功能换取安全：Haskell 语言证明了两者皆有可能。

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

此外，Haskell 类型系统及其默认的惰性和纯粹的编码方法可以帮助您处理复杂但重要的问题，例如并行性和并发性。

只是我的两分钱。

回复收藏 0 原文

携君以终年 2024-10-01 15:43:25

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

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

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

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

One thing I really like and miss in other languages is the support of typclasses, which are an elegant solution for many problems (including for instance polyvariadic functions).

Using typeclasses, it's extremely easy to define very abstract functions, which are still completely type-safe - like for instance this Fibonacci-function:

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

For instance:

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

You may even define your own numeric type for this.

回复收藏 0 原文

分开我的手 2024-10-01 15:43:25

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

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