存在类型如何与路径依赖类型重叠? [英] How do existential types overlap with path-dependent types?

问题描述

启动 Scala 3 存在类型已删除原因之一是

Starting Scala 3 existential types have been dropped and one of the reasons is stated as

存在类型与路径依赖类型在很大程度上重叠，所以拥有它们的收益相对较小.

Existential types largely overlap with path-dependent types, so the gain of having them is relatively minor.

鉴于很大程度上"，所以并非总是如此，我想知道是否可以提供一个具体的示例来演示如何将存在类型重写为路径依赖类型，以及一个无法进行此类替换的示例?

Given "largely", so not always, I was wondering if a concrete example can be provided demonstrating how to rewrite an existential type as path-dependent type, and an example when such replacement is not possible?

推荐答案

假设 T 是我们要通过存在量词绑定的类型，并且 F[T] 是某种依赖于 T 的类型，所以

Suppose that T is the type we want to bind by the existential quantifier, and F[T] is some type that depends on T, so that

type A = F[T] forSome { type T }

是我们的存在类型.

提供类型 A 的实例意味着:

Providing an instance of type A means that:

• 存在某种类型 t 可以被 T
绑定
• 存在 F[t]
类型的值

• there exists some type t that can be bound by T
• there exists a value of type F[t]

但我们也可以将两个组件放在一个类型中，并使 T 成为依赖于路径的类型成员:

But we could just as well put both components into a single type, and make T a path-dependent type member:

type B = { type T; val value: F[T] }

B 类型的实例由相同的数据描述:

Instances of type B are described by same data:

• 某些类型 t 可以通过名称 T 绑定.
• F[t]
类型的值

• Some type t that can be bound by the name T.
• A value of type F[t]

A 和 B 的值携带大致相同的信息，主要区别在于我们如何访问类型 T我们正在量化.对于b:B，我们可以将其作为路径依赖类型pT，而对于a:A，我们可以使用类型-模式匹配中的变量.

The values of both A and B carry around roughly the same information, the main difference is how we can access the type T over which we are quantifying. In case of b: B, we can get it as path-dependent type p.T, whereas for a: A, we could use type-variables in pattern matching.

这是一个示例，演示了如何在存在量化类型和路径依赖类型之间进行映射:

Here is an example that demonstrates how to map between the existentially quantified and the path dependent types:

def example[F[_]]: Unit = {
  type A = F[T] forSome { type T }
  type B = { type T; val value: F[T] }
  def ex2pd(a: A): B = a match {
    case v: F[t] => new { type T = t; val value = v }
  }
  def pd2ex(b: B): A = b.value
}

(在 2.13 上编译)

(this compiles on 2.13)

我猜很大程度上"是在那里，因为与 Scala 3/Dotty 不同，以前的 Scala 版本没有任何严格形式化的基础，所以这句话的作者可能只是不想引起这样的印象，即 2.13 中的每个存在类型都可以由路径依赖来精确表示类型，因为这样的声明无论如何都不能严格.

I would guess that the "largely" is there, because unlike Scala 3 / Dotty, previous versions of Scala did not have any rigorously formalized foundations, so maybe the author of this sentence just did not want to invoke the impression that every existential type from 2.13 could be exactly represented by path dependent types, because such a claim could not be made rigorous anyway.

这篇关于存在类型如何与路径依赖类型重叠?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！