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@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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe