Adds a linear fat arrow %1 => this is meant to greatly improve the ergonomics of some of the APIs using linear types (it tends to apply to APIs based on typestate or related to mutation).
@jaror will this interact with any future proposals towards DH? I’m worried that this increase the pile of chores one would have to do to finally reach the goal of implementing them, similarly to how it happened with LinearTypes (and multiplicity polymorphism ftm) themselves.
The changes seem pretty modest as the costs and drawbacks section also says. But I wouldn't know how complicated it is to combine normal constraints with dependent types, let alone linear constraints.
@jaror yeah it seems fine at first; issue is that someone probably has to do the theory part, writing a new papers for every one new addition seems tedious 😅
Add comment