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

[David Feuer]

 I have heard of this "eta rule" before, but I know nothing about type
theory. What does the rule say?

On Tue, Apr 12, 2016 at 3:41 AM, Adam Gundry <adam at well-typed.com> wrote:
> 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/
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe