[haskellandchill]

I'm trying to understand why dependent types can't represent linearity since you can model Nat at type level in dependent types. Dependent types can do capability modeling at the type level and linearity (or affinity) seems like a capability. From this thread (https://www.reddit.com/r/haskell/comments/20k4ei/do_dependen...) it seems like it can be done. I'm looking for something more formal to explain the orthogonality (or simulatability) of linear types inside a dependent type system.

[chriswarbo]

From my understanding, dependent types can model linearity, but you'd need to use that model type system rather than the 'native' type system (similar to how, for example, Bash can model OOP (e.g. using a mixture of naming conventions, associative arrays, eval, etc.), but isn't natively OOP). If we go down that route, we're essentially building our own programming language, which is inherently incompatible with the dependently-typed language we've used to create it (in particular: functions in the underlying language cannot be used in our linear-types language, since they have no linearity constraints).

A common example is a file handle: I can prove that the 'close' function will produce a closed handle, e.g.

    close : Handle Open -> Handle Closed

I can prove that those handles point to the same file:

    close : (f: Filename) -> Handle f Open -> Handle f Closed

I can prove arbitrary relationships between the input values and the output value. Yet nothing I do restrict the structure of a term, like how many times a variable is used, to prevent e.g.

    foo h = snd (close h, readLine h)

For that sort of control, we need to build the ability to track things into the term language itself; either by adding linear types (or equivalent) to the language, or building a new incompatible language on top (as I mentioned above).

[haskellandchill]

Cool. Actually I should know more about this since I took a lecture series with Krishnaswami on this topic. He combines the two type systems in a way that makes sense and can produce a programming language.

But yes, for the linearity control you'd need to model variables within the type system and indirect to a function handling h's resource relationship instead of using it directly.

Formally I would like to compare linear types and dependent types and their ability to encode or not each other. I don't know what the tools for that are.