[jlrubin]

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".

[gavinray]

Scala 3 is the only "functional" language that made me not feel like an idiot, and it's great for understanding "Dependent Types" as a layman.

It gives the example of a key in a database, which can return multiple types of values:

  type DB = (k: Key) => Option[k.Value]

Where the type of "Key" is:

  trait Key { type Value }

You can declare generic values of type "Key[Value]" and attempting to look them up in the DB can result in more than one kind of type, dependent on the value being looked up.

https://docs.scala-lang.org/scala3/book/types-dependent-func...

[DylanSp]

I wouldn't call those dependent types, exactly, because it's still happening entirely at the type level. The defining characteristic of dependent type systems is that they allow mixing of type-level and value-level expressions. To use the classic example of appending one vector to another, Idris lets us express the type:

  app : Vect n a -> Vect m a -> Vect (n + m) a

where we're using the value-level addition operator to express the type of the result; specifically, that appending a Vect of length m to a Vect of length n will give a Vect of length (n + m). [1]

[1] Taken from https://www.idris-lang.org/pages/example.html

[dwohnitmok]

They are dependent types since they do depend on runtime values (notice in `DB` the `k` is a runtime value), rather than just types. They are, however, very restricted compared to more "full-spectrum" dependently typed languages.

[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.

[dwohnitmok]

If Scala syntax is more up your alley, here's an intro to dependent types that has more Scala-esque syntax: https://shuangrimu.com/posts/language-agnostic-intro-to-depe...

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).

[exdsq]

A really nice thing in Haskell beyond dependent types is refinement types. Not sure if they exist in Scala - I'm sure someone has hacked something together somewhere.

https://ucsd-progsys.github.io/liquidhaskell-blog/

[ozmaverick72]

Yip you are right I got that screwed up.