you got it flipped. Dependendent types enable you to do things like "takes a nonempty list" and "returns a nonempty list of greater size".
Linear types lets you do things like "this data can only be written to a file once".
Linear types lets you do things like "this data can only be written to a file once".
It gives the example of a key in a database, which can return multiple types of values:
type DB = (k: Key) => Option[k.Value]
trait Key { type Value }
https://docs.scala-lang.org/scala3/book/types-dependent-func...
interface Key<V> { ... }
class Name extends Key<String> { ... }
class Age extends Key<Integer> { ... }
interface DB {
public <V> Optional<V> get(Key<V> k) { ... }
} Name nameKey = ...;
Age ageKey = ...;
Optional<String> name = db.get(nameKey);
Optional<Integer> age = db.get(ageKey);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.
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)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] = ...
<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>) { ... }
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.
app : Vect n a -> Vect m a -> Vect (n + m) a
[1] Taken from https://www.idris-lang.org/pages/example.html
Scala has only a very limited version of dependent types. Even its "dependent function types" are a more restricted version of general dependent function types. Full dependent types can in a certain sense be even simpler than non-dependently-typed languages (e.g. you no longer need a separate notion of generics).