[Haskell-cafe] Is there a type class for boring types?

[David Feuer]

Indeed! Empty is lucky. The existence, for a type x, of a function

impossible :: forall y . x -> y

is sufficient--parametricity guarantees uniqueness. For Boring/Singular,
this is certainly not the case. Non-boring types y typically have multiple
functions

possible :: forall x . x -> y

We'd really want

sole :: Pi (y :: a) -> inhabitant = y

For some horrifyingly vague notion of equality. That obviously isn't going
to cut it for real Haskell.
On Feb 2, 2016 4:34 PM, "Tom Ellis" <
tom-lists-haskell-cafe-2013 at jaguarpaw.co.uk> wrote:

> On Tue, Feb 02, 2016 at 12:41:34PM -0500, David Feuer wrote:
> > Or, alternatively, some common class that lets me express that a type is
> > boring (i.e., inhabited by precisely one fully-defined value)?
>
> FWIW it's the dual of Empty:
>
>
> https://hackage.haskell.org/package/total-1.0.4/docs/Lens-Family-Total.html
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160202/91a04622/attachment.html>