<p dir="ltr">Indeed! Empty is lucky. The existence, for a type x, of a function</p>
<p dir="ltr">impossible :: forall y . x -> y</p>
<p dir="ltr">is sufficient--parametricity guarantees uniqueness. For Boring/Singular, this is certainly not the case. Non-boring types y typically have multiple functions</p>
<p dir="ltr">possible :: forall x . x -> y</p>
<p dir="ltr">We'd really want</p>
<p dir="ltr">sole :: Pi (y :: a) -> inhabitant = y</p>
<p dir="ltr">For some horrifyingly vague notion of equality. That obviously isn't going to cut it for real Haskell.</p>
<div class="gmail_quote">On Feb 2, 2016 4:34 PM, "Tom Ellis" <<a href="mailto:tom-lists-haskell-cafe-2013@jaguarpaw.co.uk">tom-lists-haskell-cafe-2013@jaguarpaw.co.uk</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On Tue, Feb 02, 2016 at 12:41:34PM -0500, David Feuer wrote:<br>
> Or, alternatively, some common class that lets me express that a type is<br>
> boring (i.e., inhabited by precisely one fully-defined value)?<br>
<br>
FWIW it's the dual of Empty:<br>
<br>
    <a href="https://hackage.haskell.org/package/total-1.0.4/docs/Lens-Family-Total.html" rel="noreferrer" target="_blank">https://hackage.haskell.org/package/total-1.0.4/docs/Lens-Family-Total.html</a><br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
</blockquote></div>