<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">But we morally *do* have explicit kind application. See accepted proposal <a href="https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0015-type-level-type-applications.rst" class="">https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0015-type-level-type-applications.rst</a> So the only reason that we don't have it is that GHC hasn't caught up to its specification. (I have a student working on this now.)<div class=""><br class=""></div><div class="">The reason that T2 and T3 are different here is that T2 mentions the k in the type declaration, while T3 mentions it only in the constructor declaration.</div><div class=""><br class=""></div><div class="">Richard<br class=""><div class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Jun 26, 2018, at 6:52 PM, Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" class="">iavor.diatchki@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">Hello,<div class="">thanks for the revisions---I read through the new version, and I think I almost understand the plan. I would say that for this proposal it makes more sense to just deal with explicit specificities at the value level, and never have the curly braces in type constructors. Since we don't have an explicit kind application at the type level (e.g., we can't write `Proxy @Type`), I don't think it really makes sense to add the braces to type constructors. If we ever implemented THAT feature, then we can discuss which declarations should have explicit and which should have implicit parameters. In the current set of examples, I find it odd that `T2` does not have braces, but `T3` does.</div><div class=""><br class=""></div><div class="">-Iavor</div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""></div></div><br class=""><div class="gmail_quote"><div dir="ltr" class="">On Wed, Jun 20, 2018 at 2:15 PM Richard Eisenberg <<a href="mailto:rae@cs.brynmawr.edu" class="">rae@cs.brynmawr.edu</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space" class="">I have posted the new proposal, at <a href="https://github.com/ghc-proposals/ghc-proposals/pull/148" target="_blank" class="">https://github.com/ghc-proposals/ghc-proposals/pull/148</a><div class=""><br class=""></div><div class="">I've also updated #99 to clarify where the new syntax is allowed.</div><div class=""><br class=""></div><div class="">For Iavor's examples: </div><div class=""><div class=""><br class=""></div><div class=""></div></div></div><div style="word-wrap:break-word;line-break:after-white-space" class=""><div class=""><div class=""><blockquote type="cite" class=""><div dir="ltr" class=""><div class=""><div class="">data T1 a = C1 a</div></div></div></blockquote><div class=""><br class=""></div></div></div></div><div style="word-wrap:break-word;line-break:after-white-space" class=""><div class=""><div class=""><div class="">type T1 :: Type -> Type</div><div class="">C1 :: forall a. a -> T1 a</div></div></div></div><div style="word-wrap:break-word;line-break:after-white-space" class=""><div class=""><div class=""><br class=""><blockquote type="cite" class=""><div dir="ltr" class=""><div class=""><div class="">data T2 (a :: k) = C2 { f2 :: Proxy a }</div></div></div></blockquote><div class=""><br class=""></div></div></div></div><div style="word-wrap:break-word;line-break:after-white-space" class=""><div class=""><div class=""><div class="">type T2 :: forall k. k -> Type</div><div class="">C2 :: forall k (a :: k). Proxy a -> T2 a</div><div class="">f2 :: forall k (a :: k). T2 a -> Proxy a</div></div></div></div><div style="word-wrap:break-word;line-break:after-white-space" class=""><div class=""><div class=""><br class=""><blockquote type="cite" class=""><div dir="ltr" class=""><div class=""><div class="">data T3 a where C3 :: forall k (a::k). Proxy a -> T3 a</div></div></div></blockquote><div class=""><br class=""></div></div></div></div><div style="word-wrap:break-word;line-break:after-white-space" class=""><div class=""><div class=""><div class="">type T3 :: forall {k}. k -> Type</div></div></div></div><div style="word-wrap:break-word;line-break:after-white-space" class=""><div class=""><div class=""><div class="">C3 :: forall k (a :: k). Proxy a -> T3 a</div><br class=""><blockquote type="cite" class=""><div dir="ltr" class=""><div class=""><div class="">data T4 a where C4 :: forall {k} (a::k). Proxy a -> T3 a</div></div></div></blockquote><div class=""><br class=""></div></div></div></div><div style="word-wrap:break-word;line-break:after-white-space" class=""><div class=""><div class=""><div class="">type T4 :: forall {k}. k -> Type</div></div></div></div><div style="word-wrap:break-word;line-break:after-white-space" class=""><div class=""><div class=""><div class="">C4 :: forall {k} (a :: k). Proxy a -> T3 a</div><br class=""><blockquote type="cite" class=""><div dir="ltr" class=""><div class=""><div class="">data T5 k a where C5 :: forall k (a::k). Proxy a -> T5 k a</div></div></div></blockquote><div class=""><br class=""></div></div></div></div><div style="word-wrap:break-word;line-break:after-white-space" class=""><div class=""><div class=""><div class="">Rejected, as k is used dependently but is not lexically dependent. (This is no change.) It we have</div><div class=""><br class=""></div><div class="">> data T5 k (a :: k) where C5 :: forall k (a :: k). Proxy a -> T5 k a</div><div class=""><br class=""></div><div class="">we would get</div><div class=""><br class=""></div><div class="">type T5 :: forall k -> k -> Type</div></div></div></div><div style="word-wrap:break-word;line-break:after-white-space" class=""><div class=""><div class=""><div class="">C5 :: forall k (a :: k). Proxy a -> T5 k a</div><br class=""><blockquote type="cite" class=""><div dir="ltr" class=""><div class=""><div class="">data T6 k a where C6 :: forall {k} (a::k). Proxy a -> T6 k a</div></div></div></blockquote></div></div></div><div style="word-wrap:break-word;line-break:after-white-space" class=""><div class=""><div class=""><div class=""><div dir="ltr" class=""><div class=""><div class=""><br class=""></div><div class="">Rejected, like T6. If we revise to:</div><div class=""><br class=""></div><div class="">> data T6 k (a :: k) where C6 :: forall {k} (a::k). Proxy a -> T6 k a</div><div class=""><br class=""></div><div class="">we get</div><div class=""><br class=""></div><div class="">type T6 :: forall k -> k -> Type</div></div></div></div></div></div></div><div style="word-wrap:break-word;line-break:after-white-space" class=""><div class=""><div class=""><div class=""><div dir="ltr" class=""><div class=""><div class="">C6 :: forall {k} (a::k). Proxy a -> T6 k a</div><div class=""><br class=""></div></div></div></div></div></div></div><div style="word-wrap:break-word;line-break:after-white-space" class=""><div class=""><div class=""><div class=""><div dir="ltr" class=""><div class=""><div class="">I've updated the proposal itself to include these examples.</div><div class=""><br class=""></div><div class="">Does this help to clarify?</div></div></div></div></div></div></div><div style="word-wrap:break-word;line-break:after-white-space" class=""><div class=""><div class=""><div class=""><div dir="ltr" class=""><div class=""><div class=""><br class=""></div><div class="">Richard</div></div></div></div></div></div></div><div style="word-wrap:break-word;line-break:after-white-space" class=""><div class=""><div class=""><br class=""><blockquote type="cite" class=""><div class="">On May 25, 2018, at 1:56 PM, Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" target="_blank" class="">iavor.diatchki@gmail.com</a>> wrote:</div><br class="m_-6255680490502056640Apple-interchange-newline"><div class=""><div dir="ltr" class="">Hello,<div class=""><br class=""></div><div class="">well, I thought that Richard was going to write a new proposal based on the feedback here, but it sounds like he is planning to revise #99, and then write a separate new one. I guess we should discuss the proposal again once the changes are in. I would encourage Richard to add some text and examples to clarify exactly what's in the proposal and what's not, and how things are supposed to work. Here are some examples, for which it would be illuminating (to me) to see the types/kinds of all names introduced.</div><div class=""><br class=""></div><div class=""><div class="">data T1 a = C1 a</div><div class="">data T2 (a :: k) = C2 { f2 :: Proxy a }</div><div class="">data T3 a where C3 :: forall k (a::k). Proxy a -> T3 a</div><div class="">data T4 a where C4 :: forall {k} (a::k). Proxy a -> T3 a</div><div class="">data T5 k a where C5 :: forall k (a::k). Proxy a -> T5 k a</div><div class="">data T6 k a where C6 :: forall {k} (a::k). Proxy a -> T6 k a</div></div><div class=""><br class=""></div><div class="">-Iavor</div><div class=""><br class=""></div><br class=""><div class="gmail_quote"><div dir="ltr" class="">On Fri, May 25, 2018 at 2:02 AM Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com" target="_blank" class="">simonpj@microsoft.com</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div lang="EN-GB" link="blue" vlink="purple" class="">
<div class="m_-6255680490502056640m_-4749116994332586989m_463251841758833202WordSection1"><p class="MsoNormal"><span style="font-size:12.0pt" class="">I’m keen to get #99 into GHC in some form.
<u class=""></u><u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""><u class=""></u> <u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class="">My motivation (which could be a fourth bullet in the proposal) is that it should be possible for a programmer to write a fully-explicit type signature for anything GHC can infer. But currently we can’t.
For typeRep1 GHC infers the signature shown for typeRep3; but we can’t write it down.<u class=""></u><u class=""></u></span></p></div></div><div lang="EN-GB" link="blue" vlink="purple" class=""><div class="m_-6255680490502056640m_-4749116994332586989m_463251841758833202WordSection1"><p class="MsoNormal"><span style="font-size:12.0pt" class=""><u class=""></u> <u class=""></u></span></p><p class="MsoNormal" style="margin-left:36.0pt">based on the discussion so far, it seems that #99 in its current form might not be exactly what we want<u class=""></u><u class=""></u></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""><u class=""></u> <u class=""></u></span></p>
</div></div><div lang="EN-GB" link="blue" vlink="purple" class=""><div class="m_-6255680490502056640m_-4749116994332586989m_463251841758833202WordSection1"><p class="MsoNormal"><span style="font-size:12.0pt" class="">Can you summarise the reasons it might not be exactly what we want?<u class=""></u><u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""><u class=""></u> <u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class="">Simon<u class=""></u><u class=""></u></span></p><p class="MsoNormal"><span style="font-size:12.0pt" class=""><u class=""></u> <u class=""></u></span></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt" class="">
<div class="">
<div style="border:none;border-top:solid #e1e1e1 1.0pt;padding:3.0pt 0cm 0cm 0cm" class=""><p class="MsoNormal"><b class=""><span lang="EN-US" class="">From:</span></b><span lang="EN-US" class=""> ghc-steering-committee <<a href="mailto:ghc-steering-committee-bounces@haskell.org" target="_blank" class="">ghc-steering-committee-bounces@haskell.org</a>>
<b class="">On Behalf Of </b>Richard Eisenberg<br class="">
<b class="">Sent:</b> 24 May 2018 21:17<br class="">
<b class="">To:</b> Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" target="_blank" class="">iavor.diatchki@gmail.com</a>><br class="">
<b class="">Cc:</b> <a href="mailto:ghc-steering-committee@haskell.org" target="_blank" class="">ghc-steering-committee@haskell.org</a>; Joachim Breitner <<a href="mailto:mail@joachim-breitner.de" target="_blank" class="">mail@joachim-breitner.de</a>><br class="">
<b class="">Subject:</b> Re: [ghc-steering-committee] Discussion on proposal #99: forall {k}<u class=""></u><u class=""></u></span></p>
</div>
</div></div></div></div><div lang="EN-GB" link="blue" vlink="purple" class=""><div class="m_-6255680490502056640m_-4749116994332586989m_463251841758833202WordSection1"><div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt" class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p><p class="MsoNormal">I do plan on turning Joachim's recent suggestion into a separate proposal, and then to modify #99. But the modification would remove only the bit about classes, not the feature overall. I don't have time to do this now, though -- will do
next week.<u class=""></u><u class=""></u></p>
<div class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal">Richard<u class=""></u><u class=""></u></p>
<div class=""><p class="MsoNormal"><br class="">
<br class="">
<u class=""></u><u class=""></u></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt" class="">
<div class=""><p class="MsoNormal">On May 24, 2018, at 1:54 PM, Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" target="_blank" class="">iavor.diatchki@gmail.com</a>> wrote:<u class=""></u><u class=""></u></p>
</div><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
<div class="">
<div class=""><p class="MsoNormal">Hello,<u class=""></u><u class=""></u></p>
<div class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal">based on the discussion so far, it seems that #99 in its current form might not be exactly what we want, so I'd say that we should reject it for the moment. Overall, I agree that it would be nice to come up with a consistent notation
for things that are currently happening in GHC but we can't write, so perhaps we could revisit this with a revised proposal at a later time?<u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal">-Iavor<u class=""></u><u class=""></u></p>
</div>
<div class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
<div class=""><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
</div><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
<div class="">
<div class=""><p class="MsoNormal">On Sat, May 5, 2018 at 8:48 PM Joachim Breitner <<a href="mailto:mail@joachim-breitner.de" target="_blank" class="">mail@joachim-breitner.de</a>> wrote:<u class=""></u><u class=""></u></p>
</div>
<blockquote style="border:none;border-left:solid #cccccc 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm" class=""><p class="MsoNormal">Hi,<br class="">
<br class="">
Am Mittwoch, den 02.05.2018, 16:10 -0400 schrieb Richard Eisenberg:<br class="">
> Joachim, you are always a fount of interesting ideas.<br class="">
> <br class="">
> > On May 2, 2018, at 2:51 PM, Joachim Breitner <mail@joachim-breitner<br class="">
> > .de> wrote:<br class="">
> > <br class="">
> > class C k (a : k) where meth :: a<br class="">
> > meth :: forall {k} a. C k a -> k -> Constraint<br class="">
> <br class="">
> I think this is brilliant. But not only for this proposal! Imagine<br class="">
> this:<br class="">
> <br class="">
> class Num a where<br class="">
> fromInteger :: Integer -> a<br class="">
> <br class="">
> fromInteger :: Integer -> forall a. Num a => a<br class="">
> <br class="">
> If we do that, then #129 is essentially solved, at no further cost to<br class="">
> anyone. (Note that in all Haskell98-style code, no one will ever be<br class="">
> able to notice the changed type of fromInteger.)<br class="">
> <br class="">
> This approach also allows for the possibility of reordering<br class="">
> quantified type variables for Haskell98-style constructors, if anyone<br class="">
> should want to do it.<br class="">
> <br class="">
> And it allows for updated types (including quantified variable<br class="">
> ordering, etc.) for record selectors.<br class="">
> <br class="">
> And it allows (maybe?) for giving good types to GADT record<br class="">
> selectors:<br class="">
> <br class="">
> data X a where<br class="">
> Foo :: { bar :: Int } -> X Int<br class="">
> Quux :: { bar :: Bool } -> X Bool<br class="">
> bar :: X a -> a<br class="">
> <br class="">
> GHC currently rejects the declaration for X, but it could be accepted<br class="">
> if only we could specify the correct type of bar. And now we can. I<br class="">
> don't particularly want to cook up the typing rules here, but I don't<br class="">
> think I'm totally crazy.<br class="">
> <br class="">
> GADT record selectors aside, the rule for these could be that the<br class="">
> top-level type signature must be equivalent w.r.t. the subtype<br class="">
> relation with the original type signature. That is, if the new<br class="">
> signature is t1 and the old was t2, then t1 <: t2 and t2 <: t1. Easy<br class="">
> enough to check for. The implementation would probably do a little<br class="">
> worker/wrapper stunt.<br class="">
<br class="">
I smell a new proposal… what does this mean for #99? Will you want to<br class="">
revise it?<br class="">
<br class="">
Cheers,<br class="">
Joachim<br class="">
-- <br class="">
Joachim Breitner<br class="">
<a href="mailto:mail@joachim-breitner.de" target="_blank" class="">mail@joachim-breitner.de</a><br class="">
<a href="https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim-breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7Ca43c362fd18e4163aeba08d5c1b34be2%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636627898179266033&sdata=1cwPEVKXCcP3DuCHXOFuA%2BbEBniRLjcKI%2BAZji5vR4Q%3D&reserved=0" target="_blank" class="">
http://www.joachim-breitner.de/</a><br class="">
_______________________________________________<br class="">
ghc-steering-committee mailing list<br class="">
<a href="mailto:ghc-steering-committee@haskell.org" target="_blank" class="">ghc-steering-committee@haskell.org</a><br class="">
<a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" target="_blank" class="">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><u class=""></u><u class=""></u></p>
</blockquote>
</div><p class="MsoNormal">_______________________________________________<br class="">
ghc-steering-committee mailing list<br class="">
<a href="mailto:ghc-steering-committee@haskell.org" target="_blank" class="">ghc-steering-committee@haskell.org</a><br class="">
<a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" target="_blank" class="">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><u class=""></u><u class=""></u></p>
</div>
</blockquote>
</div><p class="MsoNormal"><u class=""></u> <u class=""></u></p>
</div>
</div></div></div></blockquote></div></div>
</div></blockquote></div><br class=""></div></div></blockquote></div>
</div></blockquote></div><br class=""></div></div></body></html>