Serokell’s Work on GHC: Dependent Types, Part 5

查看原文 / View Original 编辑 / Edit

Serokell’s Work on GHC: Dependent Types, Part 5

Serokell 在 GHC 上的工作：依赖类型，第五部分

This article continues the fine tradition of Serokell’s GHC team sharing their progress on bringing dependent types to Haskell. A lot has happened since the last report, and there is plenty to cover. In this edition, Vladislav Zavialov presents three major contributions and a host of smaller improvements that push Dependent Haskell closer to becoming a practical reality. 本文延续了 Serokell GHC 团队分享其在 Haskell 中引入依赖类型进展的优良传统。自上次报告以来，发生了许多变化，内容非常丰富。在本期中，Vladislav Zavialov 展示了三项重大贡献以及一系列较小的改进，这些改进使“依赖 Haskell”（Dependent Haskell）离成为现实更近了一步。

Summary

摘要

The highlights of this report are: 本报告的重点包括：

  • Visible forall in GADTs
  • GADT 中的可见 forall
  • Namespace-specified imports
  • 命名空间指定的导入
  • Type instances in kind checking
  • 种类检查（kind checking）中的类型实例

After that, we are going to go through a number of other improvements: 此后，我们将介绍其他一些改进：

  • Progress on unifying HsType and HsExpr
  • 统一 HsType 和 HsExpr 的进展
  • The star kind syntax in required type arguments
  • 必需类型参数中的星号种类（star kind）语法
  • Pun detection in required type arguments
  • 必需类型参数中的双关语（pun）检测
  • New type families: Tuple, Constraints, Tuple#, Sum#
  • 新的类型族：Tuple, Constraints, Tuple#, Sum#
  • Rework of name resolution for built-in and punned names
  • 重构内置名称和双关名称的解析

Visible forall in GADTs

GADT 中的可见 forall

The design of dependent types for Haskell, as described by GHC Proposal #378 “Design for Dependent Types”, includes support for at least 6 quantifiers: 正如 GHC 提案 #378“依赖类型设计”中所述，Haskell 的依赖类型设计包括对至少 6 种量词的支持：

QuantifierDependenceVisibilityErasure
量词依赖性可见性擦除
forall a. tyDependentInvisibleErased
forall a -> tyDependentVisibleErased
foreach a. tyDependentInvisibleRetained
foreach a -> tyDependentVisibleRetained
Eq a => tyNon-dependentInvisibleRetained
t1 -> t2Non-dependentVisibleRetained

The one we all care about is foreach a -> ty, also known as the dependent product, dependent function, or Π-type (all three are synonymous). But before we can tackle something so ambitious, it helps to deal with the other quantifiers, such as forall a -> ty, often referred to as the visible forall or VDQ (visible dependent quantification). 我们最关心的是 foreach a -> ty，也称为依赖积、依赖函数或 Π-类型（这三者是同义词）。但在处理如此宏大的目标之前，先处理其他量词（例如 forall a -> ty，通常称为可见 forall 或 VDQ，即可见依赖量化）会更有帮助。

The majority of design questions for VDQ were resolved when GHC Proposal #281 “Visible forall in types of terms” was accepted back in 2021, and we have been relentlessly chipping away at its implementation ever since, one engineering challenge at a time. The latest advancement in this direction is the implementation of VDQ in GADTs. VDQ 的大部分设计问题在 2021 年 GHC 提案 #281“项类型中的可见 forall”被采纳时就已解决，自那时起，我们一直在不断攻克其实现过程中的每一个工程挑战。这一方向的最新进展是在 GADT 中实现了 VDQ。

Starting with GHC 9.14, the RequiredTypeArguments extension allows declarations such as the following: 从 GHC 9.14 开始，RequiredTypeArguments 扩展允许进行如下声明：

data T a where
  Typed :: forall a -> a -> T a

In this example, the Typed data constructor takes two visible arguments: a type, and then a value of that type, e.g. Typed Int 42 or Typed String "hello". This surely has a dependently-typed look to it! 在此示例中，Typed 数据构造函数接受两个可见参数：一个类型，以及该类型的一个值，例如 Typed Int 42 或 Typed String "hello"。这看起来确实很有依赖类型的样子！

One thing to keep in mind, and why this doesn’t really count as dependent types, is that the type argument is guaranteed to be erased, i.e. has no effect on how data is represented on the heap, and consequently can’t be pattern matched on: 需要记住的一点是（这也是为什么这还不算真正的依赖类型），类型参数保证会被擦除，即它对数据在堆上的表示方式没有影响，因此无法对其进行模式匹配：

f4 (Typed a x) = case a of -- Nuh-uh! This is a compile-time error
  Int -> negate x
  Bool -> not x
  _ -> x

Nonetheless, allowing this form of quantification comes with its own technical challenges, which are now behind us. This means that when it comes to adding proper dependent types, we won’t have to worry about syntactic trivia. Here is what it took to make this work. 尽管如此，允许这种形式的量化伴随着自身的技术挑战，而这些挑战现在已经被我们克服了。这意味着在添加真正的依赖类型时，我们不必再担心语法琐事。以下是实现这一功能所付出的努力。

The first challenge was that GHC’s AST for constructor patterns MkE @tp1 @tp2 p1 p2 kept the type arguments and term arguments in entirely separate lists. We refactored it to use a mixed-list representation. 第一个挑战是 GHC 用于构造函数模式 MkE @tp1 @tp2 p1 p2 的 AST 将类型参数和项参数保存在完全独立的列表中。我们对其进行了重构，使用了混合列表表示法。

The second challenge was to allow visible forall in constructor signatures. It took a few tries to get this right, as the forall-or-nothing rule that governs implicit quantification meant that some quantifiers had to be kept in a separate field. 第二个挑战是允许在构造函数签名中使用可见 forall。我们尝试了几次才将其正确实现，因为控制隐式量化的“全有或全无”（forall-or-nothing）规则意味着某些量词必须保留在单独的字段中。

The third challenge was to update the Core representation of data constructors to allow foralls of varying visibility to occur in the list of quantifiers. 第三个挑战是更新数据构造函数的 Core 表示，以允许在量词列表中出现不同可见性的 forall。

And there we have it: we are one step closer to freely mixing terms and types in our Haskell programs. Future work in that direction includes nested quantification in GADTs (#18389) and… 至此，我们离在 Haskell 程序中自由混合项和类型又近了一步。该方向的未来工作包括 GADT 中的嵌套量化 (#18389) 以及……

← 返回新闻列表 / Back to news list