<html><head><meta http-equiv="Content-Type" content="text/html charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>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.</div><div><br></div><div>Richard</div><br><div><div>On Jan 25, 2016, at 8:44 AM, David Feuer <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><p dir="ltr">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?</p>
<div class="gmail_quote">On Jan 25, 2016 7:34 AM, "Richard Eisenberg" <<a href="mailto:eir@cis.upenn.edu">eir@cis.upenn.edu</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">+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">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>
> <a href="mailto:Libraries@haskell.org">Libraries@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
<br>
</blockquote></div>
</blockquote></div><br></body></html>