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

[Iavor Diatchki]

I am not really making a proposal, but I was suggesting that it might be a
simpler way to at least start experimenting with the proposal, without
having to change the types of core Haskell concepts.

The pain of duplicating some libraries would depend on how commonly one
needs the linearity.

I do agree that it is nicer to avoid the duplication, my concern is that
the arrow story is getting quite complex. Perhaps we should view this as a
future challenge to solve and not as a blocker, I am not sure.

By the way, if this is all implemented, it would be interesting to run the
linear GHC on the standard libraries and see what types are inferred for
the various commonly used functions.

Iavor


On Tue, Aug 28, 2018, 1:49 PM Simon Peyton Jones <simonpj at microsoft.com>
wrote:

> 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.
>
>
>
> Are you proposing that pairs, lists, Maybe etc all have *non-linear*
> types?   Thus Just :: a -> Maybe a.  That would negate one of the principal
> merits of the proposal, namely that it allows all the *existing* data
> types and library functions to work for linear types too.    We don’t want
> to force people to implement carbon copies of existing libraries!
>
>
>
> I think we want both (Just :: a -o Maybe a) and (fromJust :: Maybe a -o
> a); but suppressing the lollipops when printing for the user unless
> -XLinear is on.
>
>
>
> That is, without -XLinear we behave as if the Prelude data types were
> ordinary pre-linear types; but when you switch -XLinear on, you see that
> the Prelude types are in fact linear, so that they are useful in a linear
> setting.
>
>
>
> Or am I misunderstanding the “stable middle ground”?
>
>
>
> Simon
>
>
>
> *From:* ghc-steering-committee <ghc-steering-committee-bounces at haskell.org>
> *On Behalf Of *Richard Eisenberg
> *Sent:* 27 August 2018 22:33
> *To:* Iavor Diatchki <iavor.diatchki at gmail.com>
> *Cc:* ghc-steering-committee <ghc-steering-committee at haskell.org>
> *Subject:* Re: [ghc-steering-committee] Proposal #111: Linear Types
>
>
>
> Let's keep the conversation going here. I know this is a *big* proposal,
> but we owe it to the authors to form a quorum-based consensus (I'd love
> more voices in these threads!) and offer a response.
>
>
>
> 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.
> Right now, that record would look like
>
>
>
> > data ArrowIndex = ArrowIndex { argRep :: RuntimeRep, resRep ::
> RuntimeRep }
>
> > (->) :: forall (ind :: ArrowIndex). TYPE (argRep ind) -> TYPE (resRep
> ind) -> Type
>
>
>
> With this proposal, we move up to
>
>
>
> > data ArrowIndex = ArrowIndex { argRep :: RuntimeRep, resRep ::
> RuntimeRep, multiplicity :: Multiplicity }
>
> > (->) :: forall (ind :: ArrowIndex). TYPE (argRep ind) -> TYPE (resRep
> ind) -> Type
>
>
>
> But I don't have great ideas of how to make this work syntactically --
> never mind the fact we don't have type-level records yet.
>
>
>
>
>
> 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.
>
>
>
> Richard
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20180828/73f3552d/attachment.html>