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
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