[ghc-steering-committee] A few more pleas

[Spiwack, Arnaud]

> On Dec 9, 2020, at 6:17 AM, Spiwack, Arnaud <arnaud.spiwack at tweag.io>
> wrote:
> >  Or would you rather see these stay in their standalone extensions
> forever? (which I would find, personally, rather alarming)
>
> I'm attacking from the standpoint that these will be extensions forever --
> or, at least until we have a specification of them. (Amazingly, we don't
> have a specification for either one, right now.) Haskell will always have
> new learners, and I think it's reasonable to guard some advanced features
> behind extensions, always. Perhaps we need to simplify the space of
> extensions (including a FancyTypes or DependentTypes extension), but I'd be
> happy to see these features guarded into perpetuity.
>
> About specification: The OutsideIn paper includes an overly-generous
> specification of GADTs, but not a precise one. I am unaware of a precise
> specification of what programs are accepted with GADTs, beyond the GHC
> implementation. Along similar lines, there is no specification of how type
> families reduce. (For example, what happens with `type family F where F =
> If True Int F`?)
>
This discussion is morphing into something bigger, which increasingly seems
will be a subject for the year to come (as opposed to now). There appears
to be a fairly strong divide on this subject.

> How is a partial type signature a partially-written program? Does the
> absence of type signature on a binding make a program partially written?
> Because a partial type signature is more than no signature at all, so it
> should be considered less partial at least.
>
> This is a good point. I see partial type signatures as a development tool,
> where a user elides part of a type signature in order to get the compiler
> to provide information on how to fill it in. But maybe that's not the best
> viewpoint.
>
I usually think that development tools are better handled with warnings.
That being said, if what we are looking at is elaboration, then probably
errors make sense (just like type holes make sense), though warnings work
quite well too. But if we are looking at “I’ll do this later” then warnings
are the only solution. Plus, there is a third usage of partial type
signatures which are: I really want to specify part of this type signature,
for this is where the information is (and maybe the rest is long and would
distract from the point). This latter part I use frequently in type
applications, for instance, where it is always allowed.

Maybe one of the difficulties about partial type signatures is that it is
not clear how to separate these three aspects. But I still think that
PartialTypeSignature is perfectly serviceable. And could be improved by
tuning the warning more as per this issue I once wrote and never got around
to implement.

> :set -XPartialTypeSignatures
> f :: _ -> _ ; f = (+) 1

<interactive>:3:6: warning: [-Wpartial-type-signatures]
    * Found type wildcard `_' standing for `Integer'
    * In the type `_ -> _'
      In the type signature: f :: _ -> _

<interactive>:3:11: warning: [-Wpartial-type-signatures]
    * Found type wildcard `_' standing for `Integer'
    * In the type `_ -> _'
      In the type signature: f :: _ -> _
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20201210/5f609da1/attachment.html>