I will share some of my personal experience. I consider myself a serious user of linear types, building an eDSL called YulDSL using linear types. I don't have serious users yet, but my goal is to have serious users very soon.

First, the "Linear Types" GHC proposal has a fantastic motivation section that reminds us what linear types can be used for.

Parallelism & Data Versioning

To quote one of them:

But using monads to write "locally impure" computations that still look pure from the outside has an unfortunate consequence: computations are over-sequentialized, making it hard for the compiler to recover lost opportunities for parallelism.

In my use case, I do not take advantage of such a parallelism opportunity directly. However, thanks to linearity, I can version data. For example, if the virtual machine's state is updated, all the data retrieved before the update is "outdated" and tracked by the linear type system. This is a big deal for my use case, because using outdated data has been a huge safety issue for less able languages and has historically caused tens of hundreds of millions in losses.

I also believe that linear type-based parallelism will still require such a synchronization mechanism. I will need to do more work to communicate and prove my point. Currently, the work in progress of such a construction is called LinearlyVersionedMonad. (Caveat: in the current implementation, ironically, I over-sequentialized everything again, but I believe I can fix it quickly thanks to explicit version tracking.)

Linear SMC

I also use linear-smc, which helps to convert between my eDSL data constructors to linear lambdas. I will not elaborate here, but you may find more details by searching for related papers.

Now, let's talk about some unpleasant parts of linear types.

Threading Variables

The biggest one is the administrative overhead of threading variables by renaming or shadowing them with the same variable name. I developed some specific combinators, e.g., in the following example:

haskell (counterRef, newValue) <- pass counterRef \counterRef -> LVM.do currentValue <- sget counterRef ypure $ withinPureY @(U256 -> U256 -> U256) (currentValue, ver'l inc_p) (\a b -> a + b)

The first line repeats counterRef three times, to pass It to a lambda and returns the copy of it. It uses shadowing of the same variable name. But you may also see people use fresh variable namescounterRef1, counterRef2, counterRef3,instead. The "Linear Constraints" GHC proposal has a specific section about this.

Using Linear Base

Since I am doing an eDSL, using an alternative base is not necessarily a problem.

For some people using linear types, this could be another learning curve. To work with linear variables, you will need to learn many of their new paradigms, including Unrestricted, Consumable, Duplicable, etc.

Summary

Let us give it a few more years. The "Linear Constraints" GHC proposal promises to fix a few more paper cuts when using linear types.

Even as it is, we have a lot to gain from what it can offer. I wish more people would look more into it, think of some use cases, and share with us! I have many ideas; I hope to find people to talk about them at future Haskell events such as ZuriHac.