<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>Yes, if we can arrange that Ground a implies that Equals a [a] reduces to False, with</div><div><br></div><div>type family Equals a b where</div><div> Equals a a = True</div><div> Equals a b = False</div><div><br></div><div>But getting that to work is admittedly a feature beyond what's proposed.</div><br><div><div>On Jan 25, 2016, at 9:21 AM, Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div lang="EN-GB" link="blue" vlink="purple" style="font-family: Helvetica; font-size: medium; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; "><div class="WordSection1" style="page: WordSection1; "><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "><span style="font-family: Calibri, sans-serif; ">I’m a bit dubious about whether it’s worth the effort of making this an extension that requires GHC support. Does the gain justify the (maybe-small but eternal) pain<o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "><span style="font-family: Calibri, sans-serif; "> </span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "><span style="font-family: Calibri, sans-serif; ">Simon<o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "><span style="font-family: Calibri, sans-serif; "> </span></div><div style="border-style: none none none solid; border-left-width: 1.5pt; border-left-color: blue; padding: 0cm 0cm 0cm 4pt; "><div><div style="border-style: solid none none; border-top-width: 1pt; border-top-color: rgb(225, 225, 225); padding: 3pt 0cm 0cm; "><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "><b><span lang="EN-US" style="font-size: 11pt; font-family: Calibri, sans-serif; ">From:</span></b><span lang="EN-US" style="font-size: 11pt; font-family: Calibri, sans-serif; "><span class="Apple-converted-space"> </span>ghc-devs [mailto:ghc-<a href="mailto:devs-bounces@haskell.org">devs-bounces@haskell.org</a>]<span class="Apple-converted-space"> </span><b>On Behalf Of<span class="Apple-converted-space"> </span></b>Richard Eisenberg<br><b>Sent:</b><span class="Apple-converted-space"> </span>25 January 2016 14:06<br><b>To:</b><span class="Apple-converted-space"> </span>David Feuer <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>><br><b>Cc:</b><span class="Apple-converted-space"> </span>Haskell Libraries <<a href="mailto:libraries@haskell.org">libraries@haskell.org</a>>; ghc-devs <<a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a>><br><b>Subject:</b><span class="Apple-converted-space"> </span>Re: Type class for sanity<o:p></o:p></span></div></div></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "><o:p> </o:p></div><div><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; ">Might be nice to have whnf too, while we're at it. Perhaps whnf is enough for someone and going all the way to nf would be less efficient / impossible.<o:p></o:p></div></div><div><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "><o:p> </o:p></div></div><div><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; ">Richard<o:p></o:p></div></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "><o:p> </o:p></div><div><div><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; ">On Jan 25, 2016, at 8:44 AM, David Feuer <<a href="mailto:david.feuer@gmail.com" style="color: purple; text-decoration: underline; ">david.feuer@gmail.com</a>> wrote:<o:p></o:p></div></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "><br><br><o:p></o:p></div><blockquote style="margin-top: 5pt; margin-bottom: 5pt; "><p style="margin-right: 0cm; margin-left: 0cm; font-size: 12pt; font-family: 'Times New Roman', serif; ">I don't care about the name at all. Unstuck? Would we want to distinguish between whnf (e.g., Proxy Any) and nf, or is only nf sufficiently useful?<o:p></o:p></p><div><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; ">On Jan 25, 2016 7:34 AM, "Richard Eisenberg" <<a href="mailto:eir@cis.upenn.edu" style="color: purple; text-decoration: underline; ">eir@cis.upenn.edu</a>> wrote:<o:p></o:p></div><blockquote style="border-style: none none none solid; border-left-width: 1pt; border-left-color: rgb(204, 204, 204); padding: 0cm 0cm 0cm 6pt; margin-left: 4.8pt; margin-right: 0cm; "><p class="MsoNormal" style="margin: 0cm 0cm 12pt; font-size: 12pt; font-family: 'Times New Roman', serif; ">+1<br><br>This would be very easy to implement, too.<br><br>But I suggest a different name. Ground? Terminating? NormalForm? Irreducible? ValueType? I don't love any of these, but I love Sane less.<br><br>On Jan 24, 2016, at 4:24 PM, David Feuer <<a href="mailto:david.feuer@gmail.com" style="color: purple; text-decoration: underline; ">david.feuer@gmail.com</a>> wrote:<br><br>> Since type families can be stuck, it's sometimes useful to restrict<br>> things to sane types. At present, the most convenient way I can see to<br>> do this in general is with Typeable:<br>><br>> type family Foo x where<br>> Foo 'True = Int<br>><br>> class Typeable (Foo x) => Bar x where<br>> blah :: proxy x -> Foo x<br>><br>> This will prevent anyone from producing the bogus instance<br>><br>> instance Bar 'False where<br>> blah _ = undefined<br>><br>> Unfortunately, the Typeable constraint carries runtime overhead. One<br>> possible way around this, I think, is with a class that does just<br>> sanity checking and nothing more:<br>><br>> class Sane (a :: k)<br>> instance Sane Int<br>> instance Sane Char<br>> instance Sane 'False<br>> instance Sane 'True<br>> instance Sane '[]<br>> instance Sane '(:)<br>> instance Sane (->)<br>> instance Sane 'Just<br>> instance Sane 'Nothing<br>> instance (Sane f, Sane x) => Sane (f x)<br>><br>> To really do its job properly, Sane would need to have instances for<br>> all sane types and no more. An example of an insane instance of Sane<br>> would be<br>><br>> instance Sane (a :: MyKind)<br>><br>> which would include stuck types of kind MyKind.<br>><br>> Would it be useful to add such an automatic-only class to GHC?<br>><br>> David<br>> _______________________________________________<br>> Libraries mailing list<br>><span class="Apple-converted-space"> </span><a href="mailto:Libraries@haskell.org" style="color: purple; text-decoration: underline; ">Libraries@haskell.org</a><br>><span class="Apple-converted-space"> </span><a href="https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.haskell.org%2fcgi-bin%2fmailman%2flistinfo%2flibraries&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7cdd2a26ab307a45b5f56808d32590ab5b%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=cEc6WoMyDqd3ulJ6UenlCm%2bpeYdQ4z2FMSNcXkg8Qpc%3d" target="_blank" style="color: purple; text-decoration: underline; ">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><o:p></o:p></p></blockquote></div></blockquote></div><p class="MsoNormal" style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "></p></div></div></div></blockquote></div><br></body></html>