4 ms·
How is this different from what you can do in Java? interface Key<V> { ... } class Name extends Key<String> { ... } class Age extends Key<Integer> { ...
by jhhh 5y ago
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 5y agoin 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 5y agoI 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 5y agoThe 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 5y agoIn 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 5y agoYou get a compilation error if you try that.
- dwohnitmok 5y agoYeah 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 5y agoOh, 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 5y ago> 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.