[ozmaverick72]

I had a quick read of the paper and I think I got about 10% of the content - which is better than my usual average. My take-away - linear types allow you to express conditions such as this function must not be called with an empty list - QTT types extend linear types and allow you to specify run time dependencies between functions in the type system. I got the rough idea of being able to express a state machine in the type system - gives you the ability to say that this function can only be called in this state - to enter the state, these functions must be called in this order. How did I do ? Is that the rough gist of the paper ?

[throwaway81523]

Linear logic is logic where any value must be used exactly once, i.e. if a=3 and you say b:=a, then b becomes 3 and a becomes undefined. The value is moved rather than copied. That is useful for describing e.g. resource management systems. If I transfer a resource to you, then you have it but I no longer do. Linear types basically means a type system that enforces linear logic.

A good practical description of linear logic (but not types) is here: https://hashingit.com/elements/research-resources/1994-03-Fo...

Yes it's about how Forth implements linear logic without realizing it ;).

[gadmm]

Baker's paper is visionary in that it announces a link between linear logic and move semantics for resources more than a decade in advance. As we know this was put into practice by C++ and Rust. Compared to linear types, it amounts to operating a change of perspective from the quantitative interpretation (is it copied? is it dropped?) to a qualitative one (how is it copied? how is it dropped?). This is very much in spirit of linear logic (though it takes a bit of work to relate these ideas to Girard's mathematics). It answers questions that linear types were never able to, such as how to mix linearity and control. I take this paper as an example that there is more to linear logic than linear types!

[gavinray]

Disclaimer: I'm not very bright, and don't write Idris

My understanding of "Linear Types" is that they are geared towards declaring values/types that can be used only once.

If this sounds weird, I thought so too. Except it turns out there a number of (fairly common) scenarios in which you might want to ensure that a value is only possible to be used once.

I've drank too much so I can't conjure many to mind, but what I can think of is something like a buffer in a lexer, where you want to ensure that a token is consumed once and then not available.

There are some decent examples in the Tweag repo for the GHC Linear Types proposal:

https://github.com/tweag/linear-base/tree/master/examples

[dwohnitmok]

> I've drank too much so I can't conjure many to mind

The OP has some examples. One of them is creating verified state machines (i.e. stating invariants that different states and transitions should obey all the way up to entirely specifying the abstract state machine). The paper uses linear types to replace Idris 1's ST type. Another is enforcing order of messages to be sent in a bidirectional communication protocol. There's also a lot more low-level examples (make sure that files get closed after use, make sure mutable variables are used correctly, etc.).

In general invariants of the form "verify that this happens after that happens" (and note that this phrase has two meanings which both are covered, verify that e.g. a clean up action always occurs when an action that requires clean up has happened and also verify that e.g. an action occurs after another action, and not before) can be enforced by linear types, which covers a large amount of what happens with stateful computing.

[paavohtl]

As a practical example Rust uses a less powerful version of linear types called affine types for its ownership system. Values are moved by default in assignments and function calls, and they cannot be used (in their original location) after the move.

[iopq]

Rust already has the ability to make you use the type at most once, so the useful extension for Rust would be "must-use types" which is an extension of linear types (since linear types would be able to represented in this system easily enough)

It would actually solve a lot of issues in Rust, but unfortunately would be an insane amount of work to introduce because they would invade a lot of the current type system

[paavohtl]

There is the #[must_use] attribute for function return values, which throws compiler warnings when results are unused. It is not a real part of the type system though, but it serves as a useful lint.

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

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.

[chriswarbo]

> linear types allow you to express conditions such as this function must not be called with an empty list

I don't think that's a particularly enlightening example, mostly because we can implement such a function without any linear or dependent types.

Consider that a list (of some element type T) could contain zero Ts, or one T, or two Ts, etc. i.e.

    List<T> = 1 + T + (T × T) + (T × T × T) + ...

Where:

- `1` is a type containing only one value, like 'Unit', 'Null', 'Nil, etc. We use this to represent the empty list.

- 'X + Y' is the (tagged) union of types X and Y; AKA a sum type, or an Either

- 'X × Y' is the type of tuples containing an X and a Y; AKA a product type, or a Pair

Non-empty lists are almost the same, except we don't want to allow the empty list. Hence we need to get rid of the '1' type, to get something like this:

    NonEmptyList<T> = T + (T × T) + (T × T × T) + ...

Just using the normal rules of arithmetic, we can see that NonEmptyList<T> is the same as List<T>, except everything has been multiplied by T:

    NonEmptyList<T> =          T  + (T × T) + (T × T × T) + (T × T × T × T) + ...
                    =     (T × 1) + (T × T) + (T × T × T) + (T × T × T × T) + ...
                    = T × (    1  +      T  + (    T × T) + (    T × T × T) + ...)
                    = T × List<T>

Hence we can implement NonEmptyList<T> as the type 'T × List<T>', i.e. tuples containing a T and a List<T>. Intuitively, those are the "head" and "tail" of the non-empty list; or equivalently, Cons constructs a tuple, and non-empty lists are those whose outermost constructor is always Cons.

Note that we can go the other way too, if our language provided non-empty lists and we want to allow empty ones too:

    List<T> = 1 + T + (T × T) + (T × T × T) + ...
            = 1 + NonEmptyList<T>

This time, we a value of type List<T> is either a unit value (representing the empty list), or a non-empty list. This pattern of "adding one" to a type is usually called 'Maybe' or 'Option':

    Maybe<T> = 1 + T

Hence simplifying the above to:

    List<T> = Maybe<NonEmptyList<T>>