[Haskell-cafe] Is it safe to postulate () has one inhabitant?

[Adam Gundry]

I agree that this should be safe, although it would be nice if someone
proved it! Another way to think of it is as a consequence of the eta rule:

    forall (a :: ()) . a ~ '()

There is an existing feature request [1] to add eta conversion to GHC,
which should include this.

All the best,

Adam

[1] https://ghc.haskell.org/trac/ghc/ticket/7259


On 12/04/16 01:49, Richard Eisenberg wrote:
> I believe this is safe, yes.
> 
> Saying the kind () has infinitely many types in it is somewhat like
> saying the type () has infinitely many terms in it, like (), undefined,
> undefined 1, undefined False, ... With the change to type families in
> the past few years, it should be impossible to match on any inhabitant
> of the kind () except the type '(). That makes the postulate you
> postulate quite sensible.
> 
> Richard
> 
> On Apr 11, 2016, at 4:07 PM, David Feuer <david.feuer at gmail.com
> <mailto:david.feuer at gmail.com>> wrote:
> 
>> The () kind has infinitely many inhabitants: the type '() and any
>> stuck or looping types with appropriate kinds. However, I've not been
>> able to find a way to break type safety with the postulate
>>
>> unitsEqual :: (a :: ()) :~: (b :: ())
>>
>> in GHC 7.10.3 (it was possible using a now-rejected data family in
>> 7.8.3). Is there some way I haven't found yet, or is this safe? If
>> it's *not* safe, is the equivalent postulate using Void instead of ()
>> safe? For my purposes, () would be nicer, but it feels riskier.


-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/