[Haskell-cafe] Is it safe to postulate () has one inhabitant?
david.feuer at gmail.com
Tue Apr 12 20:01:37 UTC 2016
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  to add eta conversion to GHC,
> which should include this.
> All the best,
>  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.
>> 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
More information about the Haskell-Cafe