•  29-09-2020
  •  | 
  •  

题

假设你有 3 个对象，一个全局对象 MemoryStore, ，其中有一个数组 MemorySlabCache 对象，以及每个 MemorySlabCache 有一个数组 MemorySlab 对象。 有点 像这样：

class MemoryStore {
  caches: Array<MemorySlabCache> = []
}

class MemorySlabCache {
  size: Integer
  slabs: Array<MemorySlab> = []
}

class MemorySlab {
  
}

但问题是，这并不能捕捉到一切。它还需要抓住这样一个事实：每个 MemorySlabCache 有一个尺寸，用于告诉尺寸是多少 MemorySlab 它包含的对象。所以就是 更多的 像这样：

class MemoryStore {
  caches: Array<MemorySlabCache> = []
}

class MemorySlabCache {
  size: Integer
  slabs: Array<MemorySlab<size>> = []
}

class MemorySlab<size: Integer> {
  
}

然后我们创建缓存：

let 4bytes = new MemorySlabCache(size: 4)
let 8bytes = new MemorySlabCache(size: 8)
...
let 32bytes = new MemorySlabCache(size: 32)
...
store.caches.push(4bytes, 8bytes, ..., 32bytes, ...)

这算不算“依赖型", “其定义取决于值的类型”？由于类型 Array<MemorySlab<size>> 取决于分配给的值 size 场上 MemorySlabCache. 。如果不是，这是什么？什么会使其成为依赖类型的示例？

有帮助吗？

解决方案

所以，答案可以说是“是”，这是依赖类型的一个例子。然而，人们为此创建的许多简单示例的问题在于，它们没有演示依赖类型的重要方面。

可以说你的在这方面更好，因为所讨论的类型取决于任意值 MemorySlabCache. 。然而，你从不使用 MemorySlabCache 没有静态已知值。所以一个更有趣的例子是这样的：

let cacheSize = readInteger(stdin)
store.caches.push(new MemorySlabCache(cacheSize))

因此，您允许用户在运行时选择缓存大小，但缓存大小仍然记录在类型中，并且类型检查器静态地确保所有操作相对于大小都有意义，即使大小不是静态已知的（这是你的例子的另一个问题；其中没有任何内容表明跟踪的大小随后如何重要）。

一个更小的问题是，整数是一种太容易“伪造”依赖类型的结构，因此带有它们的示例最终会低于真正的依赖类型的可行性。例如，具有某些扩展的 Haskell 甚至可以编码类似于我的运行时缓存大小示例的内容，即使它实际上没有依赖类型。您可以拥有静态已知的类型级整数，并创建一个函数，该函数根据运行时整数为您返回静态类型值的适当值。然而，基于依赖类型理论的语言通常让类型依赖于任意类型的值，例如函数类型。对于这些（以及其他相关功能），“伪造”实际上并不可行。

许可以下： CC-BY-SA 和 归因
不隶属于 cs.stackexchange
scroll top