<div dir="ltr"><div class="markdown-here-wrapper" style=""><p style="margin:0px 0px 1.2em!important"></p><div class="markdown-here-exclude"><p></p><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">> On Dec 9, 2020, at 6:17 AM, Spiwack, Arnaud <<a href="mailto:arnaud.spiwack@tweag.io" target="_blank">arnaud.spiwack@tweag.io</a>> wrote:<br>
>  Or would you rather see these stay in their standalone extensions forever? (which I would find, personally, rather alarming)<br>
<br>
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.<br>
<br>
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`?)<br></blockquote><p></p></div><p style="margin:0px 0px 1.2em!important"></p>
<p style="margin:0px 0px 1.2em!important">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.</p>
<p style="margin:0px 0px 1.2em!important"></p><div class="markdown-here-exclude"><p></p><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
> 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.<br>
<br>
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.<br></blockquote><p></p></div><p style="margin:0px 0px 1.2em!important"></p>
<p style="margin:0px 0px 1.2em!important">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.</p>
<p style="margin:0px 0px 1.2em!important">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.</p>
<pre style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;font-size:1em;line-height:1.2em;margin:1.2em 0px"><code style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px 0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px solid rgb(234,234,234);background-color:rgb(248,248,248);border-radius:3px;display:inline;white-space:pre;overflow:auto;border-radius:3px;border:1px solid rgb(204,204,204);padding:0.5em 0.7em;display:block!important">> :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 :: _ -> _
</code></pre><div title="MDH:PGRpdiBkaXI9Imx0ciIgZ21haWxfb3JpZ2luYWw9IjEiPjxicj48L2Rpdj48ZGl2IGNsYXNzPSJn
bWFpbF9xdW90ZSI+PGJsb2NrcXVvdGUgY2xhc3M9ImdtYWlsX3F1b3RlIiBzdHlsZT0ibWFyZ2lu
OiAwcHggMHB4IDBweCAwLjhleDsgYm9yZGVyLWxlZnQ6IDFweCBzb2xpZCByZ2IoMjA0LCAyMDQs
IDIwNCk7IHBhZGRpbmctbGVmdDogMWV4OyI+Jmd0OyBPbiBEZWMgOSwgMjAyMCwgYXQgNjoxNyBB
TSwgU3Bpd2FjaywgQXJuYXVkICZsdDs8YSBocmVmPSJtYWlsdG86YXJuYXVkLnNwaXdhY2tAdHdl
YWcuaW8iIHRhcmdldD0iX2JsYW5rIj5hcm5hdWQuc3Bpd2Fja0B0d2VhZy5pbzwvYT4mZ3Q7IHdy
b3RlOjxicj4KJmd0OyZuYnNwOyBPciB3b3VsZCB5b3UgcmF0aGVyIHNlZSB0aGVzZSBzdGF5IGlu
IHRoZWlyIHN0YW5kYWxvbmUgZXh0ZW5zaW9ucyBmb3JldmVyPyAod2hpY2ggSSB3b3VsZCBmaW5k
LCBwZXJzb25hbGx5LCByYXRoZXIgYWxhcm1pbmcpPGJyPgo8YnI+CkknbSBhdHRhY2tpbmcgZnJv
bSB0aGUgc3RhbmRwb2ludCB0aGF0IHRoZXNlIHdpbGwgYmUgZXh0ZW5zaW9ucyBmb3JldmVyIC0t
IG9yLCBhdCBsZWFzdCB1bnRpbCB3ZSBoYXZlIGEgc3BlY2lmaWNhdGlvbiBvZiB0aGVtLiAoQW1h
emluZ2x5LCB3ZSBkb24ndCBoYXZlIGEgc3BlY2lmaWNhdGlvbiBmb3IgZWl0aGVyIG9uZSwgcmln
aHQgbm93LikgSGFza2VsbCB3aWxsIGFsd2F5cyBoYXZlIG5ldyBsZWFybmVycywgYW5kIEkgdGhp
bmsgaXQncyByZWFzb25hYmxlIHRvIGd1YXJkIHNvbWUgYWR2YW5jZWQgZmVhdHVyZXMgYmVoaW5k
IGV4dGVuc2lvbnMsIGFsd2F5cy4gUGVyaGFwcyB3ZSBuZWVkIHRvIHNpbXBsaWZ5IHRoZSBzcGFj
ZSBvZiBleHRlbnNpb25zIChpbmNsdWRpbmcgYSBGYW5jeVR5cGVzIG9yIERlcGVuZGVudFR5cGVz
IGV4dGVuc2lvbiksIGJ1dCBJJ2QgYmUgaGFwcHkgdG8gc2VlIHRoZXNlIGZlYXR1cmVzIGd1YXJk
ZWQgaW50byBwZXJwZXR1aXR5Ljxicj4KPGJyPgpBYm91dCBzcGVjaWZpY2F0aW9uOiBUaGUgT3V0
c2lkZUluIHBhcGVyIGluY2x1ZGVzIGFuIG92ZXJseS1nZW5lcm91cyBzcGVjaWZpY2F0aW9uIG9m
IEdBRFRzLCBidXQgbm90IGEgcHJlY2lzZSBvbmUuIEkgYW0gdW5hd2FyZSBvZiBhIHByZWNpc2Ug
c3BlY2lmaWNhdGlvbiBvZiB3aGF0IHByb2dyYW1zIGFyZSBhY2NlcHRlZCB3aXRoIEdBRFRzLCBi
ZXlvbmQgdGhlIEdIQyBpbXBsZW1lbnRhdGlvbi4gQWxvbmcgc2ltaWxhciBsaW5lcywgdGhlcmUg
aXMgbm8gc3BlY2lmaWNhdGlvbiBvZiBob3cgdHlwZSBmYW1pbGllcyByZWR1Y2UuIChGb3IgZXhh
bXBsZSwgd2hhdCBoYXBwZW5zIHdpdGggYHR5cGUgZmFtaWx5IEYgd2hlcmUgRiA9IElmIFRydWUg
SW50IEZgPyk8YnI+PC9ibG9ja3F1b3RlPjxkaXY+PGJyPjwvZGl2PjxkaXY+VGhpcyBkaXNjdXNz
aW9uIGlzIG1vcnBoaW5nIGludG8gc29tZXRoaW5nIGJpZ2dlciwgd2hpY2ggaW5jcmVhc2luZ2x5
IHNlZW1zIHdpbGwgYmUgYSBzdWJqZWN0IGZvciB0aGUgeWVhciB0byBjb21lIChhcyBvcHBvc2Vk
IHRvIG5vdykuIFRoZXJlIGFwcGVhcnMgdG8gYmUgYSBmYWlybHkgc3Ryb25nIGRpdmlkZSBvbiB0
aGlzIHN1YmplY3QuPC9kaXY+PGRpdj48YnI+PC9kaXY+PGJsb2NrcXVvdGUgY2xhc3M9ImdtYWls
X3F1b3RlIiBzdHlsZT0ibWFyZ2luOiAwcHggMHB4IDBweCAwLjhleDsgYm9yZGVyLWxlZnQ6IDFw
eCBzb2xpZCByZ2IoMjA0LCAyMDQsIDIwNCk7IHBhZGRpbmctbGVmdDogMWV4OyI+CiZndDsgSG93
IGlzIGEgcGFydGlhbCB0eXBlIHNpZ25hdHVyZSBhIHBhcnRpYWxseS13cml0dGVuIHByb2dyYW0/
IERvZXMgdGhlIGFic2VuY2Ugb2YgdHlwZSBzaWduYXR1cmUgb24gYSBiaW5kaW5nIG1ha2UgYSBw
cm9ncmFtIHBhcnRpYWxseSB3cml0dGVuPyBCZWNhdXNlIGEgcGFydGlhbCB0eXBlIHNpZ25hdHVy
ZSBpcyBtb3JlIHRoYW4gbm8gc2lnbmF0dXJlIGF0IGFsbCwgc28gaXQgc2hvdWxkIGJlIGNvbnNp
ZGVyZWQgbGVzcyBwYXJ0aWFsIGF0IGxlYXN0Ljxicj4KPGJyPgpUaGlzIGlzIGEgZ29vZCBwb2lu
dC4gSSBzZWUgcGFydGlhbCB0eXBlIHNpZ25hdHVyZXMgYXMgYSBkZXZlbG9wbWVudCB0b29sLCB3
aGVyZSBhIHVzZXIgZWxpZGVzIHBhcnQgb2YgYSB0eXBlIHNpZ25hdHVyZSBpbiBvcmRlciB0byBn
ZXQgdGhlIGNvbXBpbGVyIHRvIHByb3ZpZGUgaW5mb3JtYXRpb24gb24gaG93IHRvIGZpbGwgaXQg
aW4uIEJ1dCBtYXliZSB0aGF0J3Mgbm90IHRoZSBiZXN0IHZpZXdwb2ludC48YnI+PC9ibG9ja3F1
b3RlPjxkaXY+PGJyPjwvZGl2PjxkaXY+SSB1c3VhbGx5IHRoaW5rIHRoYXQgZGV2ZWxvcG1lbnQg
dG9vbHMgYXJlIGJldHRlciBoYW5kbGVkIHdpdGggd2FybmluZ3MuIFRoYXQgYmVpbmcgc2FpZCwg
aWYgd2hhdCB3ZSBhcmUgbG9va2luZyBhdCBpcyBlbGFib3JhdGlvbiwgdGhlbiBwcm9iYWJseSBl
cnJvcnMgbWFrZSBzZW5zZSAoanVzdCBsaWtlIHR5cGUgaG9sZXMgbWFrZSBzZW5zZSksIGJ1dCB3
YXJuaW5ncyB3b3JrIHF1aXRlIHdlbGwgdG9vLiBCdXQgaWYgd2UgYXJlIGxvb2tpbmcgYXQg4oCc
SSdsbCBkbyB0aGlzIGxhdGVy4oCdIHRoZW4gd2FybmluZ3MgYXJlIHRoZSBvbmx5IHNvbHV0aW9u
LiBQbHVzLCB0aGVyZSBpcyBhIHRoaXJkIHVzYWdlIG9mIHBhcnRpYWwgdHlwZSBzaWduYXR1cmVz
IHdoaWNoIGFyZTogSSByZWFsbHkgd2FudCB0byBzcGVjaWZ5IHBhcnQgb2YgdGhpcyB0eXBlIHNp
Z25hdHVyZSwgZm9yIHRoaXMgaXMgd2hlcmUgdGhlIGluZm9ybWF0aW9uIGlzIChhbmQgbWF5YmUg
dGhlIHJlc3QgaXMgbG9uZyBhbmQgd291bGQgZGlzdHJhY3QgZnJvbSB0aGUgcG9pbnQpLiBUaGlz
IGxhdHRlciBwYXJ0IEkgdXNlIGZyZXF1ZW50bHkgaW4gdHlwZSBhcHBsaWNhdGlvbnMsIGZvciBp
bnN0YW5jZSwgd2hlcmUgaXQgaXMgYWx3YXlzIGFsbG93ZWQuPC9kaXY+PGRpdj48YnI+PC9kaXY+
PGRpdj5NYXliZSBvbmUgb2YgdGhlIGRpZmZpY3VsdGllcyBhYm91dCBwYXJ0aWFsIHR5cGUgc2ln
bmF0dXJlcyBpcyB0aGF0IGl0IGlzIG5vdCBjbGVhciBob3cgdG8gc2VwYXJhdGUgdGhlc2UgdGhy
ZWUgYXNwZWN0cy4gQnV0IEkgc3RpbGwgdGhpbmsgdGhhdCBQYXJ0aWFsVHlwZVNpZ25hdHVyZSBp
cyBwZXJmZWN0bHkgc2VydmljZWFibGUuIEFuZCBjb3VsZCBiZSBpbXByb3ZlZCBieSB0dW5pbmcg
dGhlIHdhcm5pbmcgbW9yZSBhcyBwZXIgdGhpcyBpc3N1ZSBJIG9uY2Ugd3JvdGUgYW5kIG5ldmVy
IGdvdCBhcm91bmQgdG8gaW1wbGVtZW50LjwvZGl2PjxkaXY+PGJyPjwvZGl2PjxkaXY+YGBgPGJy
PjwvZGl2PjxkaXY+Jmd0OyA6c2V0IC1YUGFydGlhbFR5cGVTaWduYXR1cmVzIDxicj4mZ3Q7IGYg
OjogXyAtJmd0OyBfIDsgZiA9ICgrKSAxPGJyPjxicj4mbHQ7aW50ZXJhY3RpdmUmZ3Q7OjM6Njog
d2FybmluZzogWzxzcGFuIHpldW00Yzg9IlBSXzdfMCIgZGF0YS1kZG53YWI9IlBSXzdfMCIgYXJp
YS1pbnZhbGlkPSJzcGVsbGluZyIgY2xhc3M9IkxJIG5nIj4tV3BhcnRpYWwtdHlwZS1zaWduYXR1
cmVzPC9zcGFuPl08YnI+Jm5ic3A7ICZuYnNwOyAqIEZvdW5kIHR5cGUgd2lsZGNhcmQgYF8nIHN0
YW5kaW5nIGZvciBgSW50ZWdlcic8YnI+Jm5ic3A7ICZuYnNwOyAqIEluIHRoZSB0eXBlIGBfIC0m
Z3Q7IF8nPGJyPiZuYnNwOyAmbmJzcDsgJm5ic3A7IEluIHRoZSB0eXBlIHNpZ25hdHVyZTogZiA6
OiBfIC0mZ3Q7IF88YnI+PGJyPiZsdDtpbnRlcmFjdGl2ZSZndDs6MzoxMTogd2FybmluZzogWzxz
cGFuIHpldW00Yzg9IlBSXzhfMCIgZGF0YS1kZG53YWI9IlBSXzhfMCIgYXJpYS1pbnZhbGlkPSJz
cGVsbGluZyIgY2xhc3M9IkxJIG5nIj4tV3BhcnRpYWwtdHlwZS1zaWduYXR1cmVzPC9zcGFuPl08
YnI+Jm5ic3A7ICZuYnNwOyAqIEZvdW5kIHR5cGUgd2lsZGNhcmQgYF8nIHN0YW5kaW5nIGZvciBg
SW50ZWdlcic8YnI+Jm5ic3A7ICZuYnNwOyAqIEluIHRoZSB0eXBlIGBfIC0mZ3Q7IF8nPGJyPiZu
YnNwOyAmbmJzcDsgJm5ic3A7IEluIHRoZSB0eXBlIHNpZ25hdHVyZTogZiA6OiBfIC0mZ3Q7IF88
L2Rpdj48ZGl2PmBgYDxicj48L2Rpdj48L2Rpdj4=" style="height:0;width:0;max-height:0;max-width:0;overflow:hidden;font-size:0em;padding:0;margin:0"></div></div></div>