[jhhh]

How is this different from what you can do in Java?

  interface Key<V> { ... }
  class Name extends Key<String> { ... }
  class Age extends Key<Integer> { ... }
  interface DB {
     public <V> Optional<V> get(Key<V> k) { ... }
  }

[drdeca]

in their example, iiuc, DB takes as input the value k, and returns a value of type Optional[k.Value] . The return type depends on the input.

[jhhh]

I could be missing something but my example does as well since it's a method level generic:

  Name nameKey = ...;
  Age ageKey = ...;
  
  Optional<String> name = db.get(nameKey);
  Optional<Integer> age = db.get(ageKey);

[Mehdi2277]

The difference is your keys are types. Dependent types are about generics where the keys are allowed to be values. You can not in Java directly do,

Optional<1> and Optional<“Name”>. You can only have types as arguments.

C++ has some dependent types in it allows you to have generic arguments be ints std::array<…, 4> but it still does not allow most values as generic type argument.

[lmm]

In that Java version someone can call get<String>(age) or get<Integer>(name). In the Scala version the value type is a member of the key.

[jhhh]

You get a compilation error if you try that.

[dwohnitmok]

Yeah the `Key` and `DB` example, while somewhat differing in semantics, can be emulated by Java.

Here's an example that extends it slightly and can't be emulated by Java.

  // I forget if I need to curry the second argument in a separate argument list
  // I'm not next to a computer with scalac at the moment, so I'll just use separate argument lists
  type DB = (k: Key) => k.IsVerified => Option[k.Value]

  trait Key {
    type Value
    val keyValue: Value
    case class IsVerified(underlyingBool: Boolean)
  }

  val myDB: DB =
    key => isVerified => x match
      case IsVerified(bool) =>
        if bool then
          // return the actual value
          doSomething()
        else
          None

  def verifyKey(key: Key): key.IsVerified =
    if isValidKey(key) then
      key.IsVerified(true)
    else
      key.IsVerified(false)

  val key0: Key = ...
  val key1: Key = ...

  val key0Verification: key0.IsVerified = verifyKey(key0)

  // Fails to compile
  // You're trying to cheat!
  // You only verified key0 and are trying to use its verification to bypass 
  // verifying key1
  myDB(key1)(key0Verification)

[lmm]

Oh, sorry, misread the generics.

In theory you can do this kind of thing in Java, but you have to give each key its own type (cumbersome because Java doesn't have singleton types) and carry the type parameters arbitrarily far back through the call graph. E.g. imagine writing a function that appends 3 type-length vectors together - in a dependently-typed language you write this as:

    def append[T, M, N, L](first: Vec[T, M], second: Vec[T, N], third: Vec[T, L]): Vec[T, M + N + L] = ...

In Java you'd have to write this as:

    <T, M, N, L, P, R> Vec<T, P> append (first: Vec<T, M>, second: Vec<T, N>, third: Vec<T, L>, isSum1: IsSum<M, N, P>, isSum2: IsSum<P, L, R>) { ... }

And as you write more and more code you have exponentially more type parameters, because you have no way to just evaluate functions of type parameters, so you have to pass markers that represent all of your type relationships right from the initial input part of your program all the way down.

[dwohnitmok]

> And as you write more and more code you have exponentially more type parameters, because you have no way to just evaluate functions of type parameters, so you have to pass markers that represent all of your type relationships right from the initial input part of your program all the way down

This isn't really the thing that dependent types provide though. If you have type-level computation without dependent types that's enough to avoid this problem (and e.g. Scala has this). However, dependent types are when the `+` in your first append is the same `+` as the usual runtime `+` rather than a separate type-level function that only works with types, not runtime values. Scala does not have this. Its dependent types are much more limited.