Re: [ghc-steering-committee] A few more pleas

On Dec 9, 2020, at 6:17 AM, Spiwack, Arnaud 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 :: _ -> _