<div dir="auto">That's what ML calls the "value restriction", right?</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Jan 22, 2023, 1:11 AM Ben Gamari <<a href="mailto:ben@smart-cactus.org">ben@smart-cactus.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div>Indeed that is the ticket.<br><br>There is one wrinkle that I should have mentioned earlier: not even all data constructor applications are admissible at the top level. In particular, constructors with strict fields may require computation to construct. The validity check would need to account for this, either by rejecting such constructors altogether or by having some of syntactic WHNF check.<br><br>Cheers,<br><br>- Ben <br><br><div class="gmail_quote">On January 21, 2023 5:06:13 PM EST, Tom Ellis <<a href="mailto:tom-lists-haskell-cafe-2017@jaguarpaw.co.uk" target="_blank" rel="noreferrer">tom-lists-haskell-cafe-2017@jaguarpaw.co.uk</a>> wrote:<blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<pre dir="auto">On Sat, Jan 21, 2023 at 10:52:33PM +0100, Jaro Reinders wrote:<br><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #729fcf;padding-left:1ex">On 21-01-2023 20:00, Ben Gamari wrote:<br><blockquote class="gmail_quote" style="margin:0pt 0pt 1ex 0.8ex;border-left:1px solid #ad7fa8;padding-left:1ex">However, I suspect you do have a point when it comes to unlifted data<br>constructors. I think it would be fine to allow an application of a<br>data constructor of an unlifted type on the top-level:<br><br>   type UMaybe :: Type -> UnliftedType<br>   data UMaybe a = UNothing | UJust a<br><br>   x :: UMaybe Int<br>   x = UJust 42<br><br>Perhaps you could open a ticket for this?<br></blockquote><br>This ticket seems related: #17521 Consider top-level unlifted bindings [1].<br><br>Or do you think it needs a separate ticket?<br></blockquote><br>Thanks Jaro.  That ticket contains the observation<br><br>"there are other cases where unlifted types are desireable at the<br> top-level (e.g. saturated data constructor applications). In<br> principle it would be fairly straightforward to incorporate a<br> validity check that admits top-level constructor applications which<br> rejecting function applications if we wanted."<br><br>So I think that ticket subsumes my question, and filing another one<br>would be redundant.<br><br>Tom<hr>Haskell-Cafe mailing list<br>To (un)subscribe, modify options or view archives go to:<br><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank" rel="noreferrer">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>Only members subscribed via the mailman list are allowed to post.</pre></blockquote></div></div>_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>