[ghc-steering-committee] Proposal #111: Linear Types

[Eric Seidel]

On Mon, Aug 27, 2018, at 17:33, Richard Eisenberg wrote:
> > On Aug 7, 2018, at 1:50 AM, Iavor Diatchki <iavor.diatchki at gmail.com> wrote:
> > The main high level concern I have is the overloading of the function space arrow.  We already have it overloaded in all kinds of ways, and adding one more dimension without any kind of underlying system seems too much.  I am not at all convinced that we will be able to "hide" multiplicities when the extension is not enabled.
> 
> I agree. I've mused about making (->) be indexed by a type-level record. 

This is diverging a bit from the actual proposal, but I'm not convinced that the record index buys us much. The various overloadings of the function arrow add syntactic overhead that a record index could alleviate, but I'd be more concerned about the cognitive overhead.

That being said, I'm less concerned about the overloading of the function arrow because Simon seems confident that we can reliably hide it when -XLinearTypes is disabled, even if datatypes are inferred linear. That makes it opt-in complexity, which I don't have a problem with.

> > Overall, while I like the core ideas, I would prefer a different way of integrating them into Haskell, one that is more modular, even at the cost of having to duplicate some code.  My reasoning is that while linearity might be useful in some cases, most of the time it is not something that we'd care about much, so we should not add it (at least straight away) to the core part of the language (functions and data types).
> 
> Is this essentially proposing that we don't make any change to 
> datatypes? That would mean that a library that wishes to have linear 
> datatypes would have to explicitly declare them as such. I think this is 
> a stable middle ground. But, if we can guarantee good error-message 
> behavior, etc., I think the "default datatypes to linear" behavior is 
> the right one.

Agreed completely.