[Haskell-cafe] Is there a type class for boring types?
david.feuer at gmail.com
Tue Feb 2 21:59:39 UTC 2016
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
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:
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe