Example of Dependent Types?

Question

Say you have 3 objects, a global MemoryStore, which has an array of MemorySlabCache objects, and each MemorySlabCache has an array of MemorySlab objects. Sort of like this:

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

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

class MemorySlab {
  
}

But the thing is, this doesn't capture everything. It also needs to capture the fact that each MemorySlabCache has a size, which is used to tell what size the MemorySlab objects are it contains. So it's more like this:

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

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

class MemorySlab<size: Integer> {
  
}

Then we create our caches:

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

Does this count as a "dependent type", "a type whose definition depends on a value"? Since the type of the Array<MemorySlab<size>> is dependent on the value assigned to the size field on MemorySlabCache. If not, what is this? What would make it into an example of dependent types?

Answer 1

So, the answer is arguably "yes," this is an example of dependent types. However, the problem with a lot of simple examples that people create for this is that they don't demonstrate non-trivial aspects of dependent typing.

Arguably yours is better in this respect, because the type in question depends on an arbitrary value in MemorySlabCache. However, you never use a MemorySlabCache without a statically known value. So a more interesting example would be like:

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

So, you allow the user to select a cache size at runtime, but the cache size is still recorded in the type, and the type checker statically ensures that all operations make sense with respect to the size, even though the size is not statically known (which is kind of another problem with your example; nothing in it shows how the tracked size matters subsequently).

A somewhat more minor problem is that integers are too easy a structure to 'fake' dependent types for, so examples with them end up under selling what might be feasible with genuine dependent types. For instance, Haskell with some extensions can encode even something similar to my runtime-cache-size example, even though it does not really have dependent types. You can have statically known type-level integers, and create a function that gives you back an appropriate value for a statically typed value based on a runtime integer. However, languages based on dependent type theory generally let types depend on values of arbitrary types, like function types. For these (and other related features), 'faking' is not really feasible.