[ghc-steering-committee] #370: Syntax for Modifiers, Recommendation: Acceptance

[Joachim Breitner]

Hi,

Am Donnerstag, den 26.11.2020, 14:58 -0500 schrieb Alejandro Serrano
Mena:
> Dear all,
> This proposal suggests adding syntax for a general notion of
> modifiers, like the ones we’ve been talking about lately affecting
> linearity or matchability of arrows. For example, if linear types and
> unsaturated families are accepted as they stand, we would have `Int
> #1 -> @U Bool` (or something like that), whereas with this proposal
> we would have the more uniform `Int %1 %Unmatchable -> Bool`.
> 
> Since the amount of modifiers is likely to increase in the future, I
> think it’s a great idea to agree and reserve such syntax, instead of
> coming up with different ways on each proposal. I thus recommend
> acceptance of this proposal.
> 
> The proposal itself:
> (1) introduces syntax for modifiers in types and defines how to
> type/kind check them,
> (2) reserved such syntax for other uses in declarations and terms.
> 
> I think the proposal still has its merits only with (1), even though
> I lean towards accepting both parts of it.

I like the idea of reserving syntax here, but parts of the proposal
smell a bit like premature generalization to me. Are we confident that
all annotations we eventually would like to use with this feature can
be expressed as types of a kind that is an instance of Modifier? Or
should we reserve the ability to have annotations that don't fit that
model?

Would we ever have annotation that may affect phases earlier than than
typechecking? What if we want to use (%type e) and (%data e) to help
with the SingleNamepace issues? Look like useful annotations to me, but
I am not sure if they fit the framework proposed here.

The fact that we special-case %1 supports that.

The proposal explicitly has to state “No modifier polymorphism!”. But
isn't that indication that using the type system to model the various
modifiers might be the wrong tool?

I wonder if there is a way where the %(…) on it’s own only reserve
syntax, and the various uses of that syntax can be disambiguated
_statically_ based on the content of …. 

Not great syntax, because not concise, enough, but morally I’d feel
more at ease with

  Int %(multiplicity Many) -> Int
  Int %(multiplicity 1) -> Int
  Int %(multiplicity m) -> Int

where multiplicity is a modifier keyword, to express the existing
features (including implicit generalization of m). Then we can extend
this to

  Int %oneShot -> Int

and

  Int %(matchability M) -> Int

and maybe even

  foo (%type [a]) -- where foo :: forall a -> ()

which is a modifier that 


So at the moment, I am inclined to reject this proposal, until I am
convinced that we are not painting ourselves into a “all modifiers are
types of special kinds and that’s all the syntax and behaviour we ever
need” corner.

Minor detail: If we can annotate infix use of the (->) “type operator”,
should we also be able to annotate other infix operators, i.e.

  constr ::= (btype | ! atype) {modifier} conop (btype | ! atype) 
  infixexp ::= lexp {modifier} qop infixexp



Cheers,
Joachim


-- 
Joachim Breitner
  mail at joachim-breitner.de
  http://www.joachim-breitner.de/