Very cool! This is exactly the topic I will probably be working in my Masters thesis. I am curious if you done anything about linearity and concurrency in the type system. Can one send files across threads for example?
Linear types can only really be used in a single-threaded manner. If multiple threads could access the same linear value, you would lose all compile time linearity guarantees, since it's out of your control in which order the threads will run.
You can transfer a linear value to another thread, but it will consume it (no longer be available) in the thread which transferred it.
If you want something with a bit more flexibility, look into Relevant types. Relevant types behave in some ways like a linear type - they disallow weakening - which means for example, if you consume it in any branch of a selection, it must be consumed in all branches. Relevant types allow contraction - unlike linear types, which means you can use them more than once - you just have to use them at least once - ie, you must ultimately consume them like you would a linear type.
You can treat Relevant types as subtypes of Linear types. If you have a value that disallows weakening, but allows contraction, you can say at any point that you are going to forbid contraction from this point onward - effectively turning it into a linear type via an upcast.
Affine types are the opposite - they allow weakening (so for example, you can use them in some branches, but not all), and in return, you are not forced to consume them - but they also cannot be used multiple times because they disallow contraction. They're use at most once. They can also be considered subtypes of Linear types - but they're a disjoint set from Relevant types.
Have a look at Granule[0], which supports these types and their interaction via a system of graded modes.
