Type Arguments in Hugs
Anthony Clayden <[email protected]> Sat, 5 Jun 2021 14:45:38 +1200
| Newsgroups | gmane.comp.lang.haskell.hugs.user |
|---|---|
| Message-ID | <CABU_mxiLEBC0G-k=-nPr7jM7wwEWBgPqG4jkUa9h2HszDM1Vug@mail.gmail.com> |
--===============7136749866038169300== Content-Type: multipart/alternative; boundary="0000000000005064c605c3fbceb6" --0000000000005064c605c3fbceb6 Content-Type: text/plain; charset="UTF-8" I'm looking on bemused as the Visible `forall` aka RequiredTypeArguments proposal goes through GHC Committee discussion. I sympathise with Simon M's alarm at the namespacing effects needed. SPJ's attempt at softening the blow: https://mail.haskell.org/pipermail/ghc-steering-committee/2021-June/002463.html > Like Simon [M], I'm sad that I have to write > f (List Int) > or > f (type [Int]) > but I think the alternative (of requiring the reader to know > the type of the function in order to resolve the binding of names > in its argument) is much, much worse. If a `type` herald is supposed to emolliate me, I have Hugs accepting this: Hugs> sizeOf (:: Int) 4 Hugs> typeOf (:: [Int]) TypeRep 3 ... * `(:: t)` -- the parens are required -- is a lot less cluttered than Proxy; * It's a little less cluttered than the proposed `type`; * More importantly, it heralds much better to my eye 'here comes a type'. I'm curious why so much of the proposal uses the `sizeOf` example. Its type currently is `Sized a => a -> Int`. It seems to me quite useful I can supply a term as argument -- I might well have in scope a (term) var of the required type. I haven't needed to change the type of `sizeOf` for the Hugs heralded syntax. The syntax is sugar for `(termType :: Int)`, in which `termType` is in effect the same as `undefined`, but with a name more revealing for diagnostics. Whereas the proposal won't actually help with `sizeOf`, until/unless the library changes its signature -- thereby breaking a load of code and dependencies. Or introduce a different-named function? The other Motivation from the proposal is to fix an inconsistency with DataKinds. It seems to me there's another way to fix such an inconsistency: change the design for DataKinds -- which to me has always been a bit of a kludge. There's also some interaction in the ugliness with `ScopedTypeVariables` -- which, with the benefit of hindsight, is increasingly getting regarded as a mis-feature. Hugs has always had the `PatternSignatures` feature, and indeed `FunctionSignatures`. It seems to me that erasure/pi-types is an implementation detail that should be kept out of the surface syntax. If the programmer wants to signal that it's the type of a term that's of concern (such that the term can be erased as well as -- ultimately -- its type), annotate the terms' position in the signature (something like with strictness), rather than banjaxing familiar syntax. Behind the scenes translate to a pi-types implementation. AntC --0000000000005064c605c3fbceb6 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable <div dir=3D"ltr">I'm looking on bemused as the Visible `forall` aka Req= uiredTypeArguments proposal goes through GHC Committee discussion. I sympat= hise with Simon M's alarm at the namespacing effects needed. SPJ's = attempt at softening the blow:<div><br></div><div><a href=3D"https://mail.h= askell.org/pipermail/ghc-steering-committee/2021-June/002463.html" target= =3D"_blank">https://mail.haskell.org/pipermail/ghc-steering-committee/2021-= June/002463.html</a><br></div><div>>=C2=A0<span style=3D"font-family:mon= ospace,monospace;color:rgb(0,0,0);font-size:1em;white-space:pre-wrap">Like = Simon [M], I'm sad that I have to write</span></div><pre style=3D"font-= size:small;white-space:pre-wrap;color:rgb(0,0,0)">> f (L= ist Int) > or > f (type [Int]) > but I think the alternative (of requiring the reader to know</pre><pre= style=3D"font-size:small;white-space:pre-wrap;color:rgb(0,0,0)">> the t= ype of the function in order to resolve the binding of names</pre><pre styl= e=3D"font-size:small;white-space:pre-wrap;color:rgb(0,0,0)">> in its arg= ument) is much, much worse.</pre><pre style=3D"font-size:small;white-space:= pre-wrap;color:rgb(0,0,0)"><br></pre><pre style=3D"font-size:small;white-sp= ace:pre-wrap;color:rgb(0,0,0)">If a `type` herald is supposed to emolliate = me, I have Hugs accepting this:</pre><pre style=3D"font-size:small;white-sp= ace:pre-wrap;color:rgb(0,0,0)">Hugs> sizeOf (:: Int)</pre><pre style=3D"= font-size:small;white-space:pre-wrap;color:rgb(0,0,0)">4</pre><pre style=3D= "font-size:small;white-space:pre-wrap;color:rgb(0,0,0)">Hugs> typeOf (::= [Int])</pre><pre style=3D"font-size:small;white-space:pre-wrap;color:rgb(0= ,0,0)">TypeRep 3 ...</pre><pre style=3D"font-size:small;white-space:pre-wra= p;color:rgb(0,0,0)"><br></pre><pre style=3D"font-size:small;white-space:pre= -wrap;color:rgb(0,0,0)">* `(:: t)` -- the parens are required -- is a lot l= ess cluttered than Proxy;</pre><pre style=3D"font-size:small;white-space:pr= e-wrap;color:rgb(0,0,0)">* It's a little less cluttered than the propos= ed `type`;</pre><pre style=3D"font-size:small;white-space:pre-wrap;color:rg= b(0,0,0)">* More importantly, it heralds much better to my eye 'here co= mes a type'.</pre><pre style=3D"font-size:small;white-space:pre-wrap;co= lor:rgb(0,0,0)"><br></pre><pre style=3D"font-size:small;white-space:pre-wra= p;color:rgb(0,0,0)">I'm curious why so much of the proposal uses the `s= izeOf` example. Its type currently is `Sized a =3D> a -> Int`. It see= ms to me quite useful I can supply a term as argument -- I might well have = in scope a (term) var of the required type.</pre><pre style=3D"font-size:sm= all;white-space:pre-wrap;color:rgb(0,0,0)">I haven't needed to change t= he type of `sizeOf` for the Hugs heralded syntax. The syntax is sugar for `= (termType :: Int)`, in which `termType` is in effect the same as `undefined= `, but with a name more revealing for diagnostics.</pre><pre style=3D"font-= size:small;white-space:pre-wrap;color:rgb(0,0,0)">Whereas the proposal won&= #39;t actually help with `sizeOf`, until/unless the library changes its sig= nature -- thereby breaking a load of code and dependencies. Or introduce a = different-named function?</pre><pre style=3D"font-size:small;white-space:pr= e-wrap;color:rgb(0,0,0)">The other Motivation from the proposal is to fix a= n inconsistency with DataKinds. It seems to me there's another way to f= ix such an inconsistency: change the design for DataKinds -- which to me ha= s always been a bit of a kludge.</pre><pre style=3D"font-size:small;white-s= pace:pre-wrap;color:rgb(0,0,0)">There's also some interaction in the ug= liness with `ScopedTypeVariables` -- which, with the benefit of hindsight, = is increasingly getting regarded as a mis-feature. Hugs has always had the = `PatternSignatures` feature, and indeed `FunctionSignatures`.</pre><pre sty= le=3D"font-size:small;white-space:pre-wrap;color:rgb(0,0,0)">It seems to me= that erasure/pi-types is an implementation detail that should be kept out = of the surface syntax. If the programmer wants to signal that it's the = type of a term that's of concern (such that the term can be erased as w= ell as -- ultimately -- its type), annotate the terms' position in the = signature (something like with strictness), rather than banjaxing familiar = syntax. Behind the scenes translate to a pi-types implementation.</pre><pre= style=3D"font-size:small;white-space:pre-wrap;color:rgb(0,0,0)"><br></pre>= <pre style=3D"font-size:small;white-space:pre-wrap;color:rgb(0,0,0)">AntC</= pre></div> --0000000000005064c605c3fbceb6-- --===============7136749866038169300== Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: base64 Content-Disposition: inline X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KSHVncy1Vc2Vy cyBtYWlsaW5nIGxpc3QKSHVncy1Vc2Vyc0BoYXNrZWxsLm9yZwpodHRwOi8vbWFpbC5oYXNrZWxs Lm9yZy9jZ2ktYmluL21haWxtYW4vbGlzdGluZm8vaHVncy11c2Vycwo= --===============7136749866038169300==--