Is it safe to postulate () has one inhabitant?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

Is it safe to postulate () has one inhabitant?

David Feuer

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.


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Is it safe to postulate () has one inhabitant?

Richard Eisenberg-2
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 <[hidden email]> 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.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Is it safe to postulate () has one inhabitant?

David Feuer

Great. My aim is to convert a poly-kinded implementation, s, of type-aligned sequences into an implementation of regular sequences by using

newtype AsUnitLoop a (x :: ()) (y :: ()) = UL  a

newtype Lower s a = Lower' (s (AsUnitLoop a) '() '())

Using the postulate, I can "prove" that

s (AsUnitLoop a) x y ~ s (AsUnitLoop a) '() '()

So when I take the tail/init of a sequence I will again get a sequence, and two sequences holding values of the same type can be concatenated. The original reflection-without-remorse code uses

data AsUnitLoop a (x :: *) (y :: *) where
  UL : a -> AsUnitLoop a () ()

which adds an extra constructor to each cell. With the postulate, I get what I want for free. I'm *hoping* it's possible to use a pattern synonym, Lower, that converts

s (AsUnitLoop a) '() '()  (requiring '())

to

Lower s a

but that provides only

exists x y . s (AsUnitLoop a) x y

when matching. This way, the postulate won't "leak" to other code unless it imports a Postulate module. Unfortunately, the pattern synonym documentation is a bit vague on types.

On Apr 11, 2016 8:49 PM, "Richard Eisenberg" <[hidden email]> 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 <[hidden email]> 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.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Is it safe to postulate () has one inhabitant?

Adam Gundry-2
In reply to this post by Richard Eisenberg-2
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 <[hidden email]
> <mailto:[hidden email]>> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> 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 <[hidden email]
>> <mailto:[hidden email]>> 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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Is it safe to postulate () has one inhabitant?

wren romano
On Tue, Apr 12, 2016 at 4:01 PM, David Feuer <[hidden email]> wrote:
>  I have heard of this "eta rule" before, but I know nothing about type
> theory. What does the rule say?

In the general use case, "eta rules" are rules that state that any
term of a given type must have a specific form defined by the
introduction and elimination rules for the type. The standard/original
version of eta is for function types:

    forall (e :: a -> b). e = (\x -> e x)

But we can generalize this to other types with a single constructor.
For example:

    forall (e :: ()). e = ()

    forall (e :: (a,b)). e = (fst e, snd e)

For any given language/theory, these various eta rules may or may not
be true. In Haskell because of decisions about un/liftedness, they
prettymuch never hold at the term level. The major counterexamples
being _|_ /= (\x -> _|_ x) and _|_ /= (fst _|_, snd _|_). Of course,
one could have eta for functions without having it for tuples, and
vice versa; there's nothing tying them together.

Getting back to the original query, the question is whether these eta
rules hold "one level up" where types must be expandable/contractible
in particular ways based on the intro/elim rules for their kind. Since
we don't have any notion of undefined at the type level, the obvious
counterexamples go away; but that still doesn't guarantee they hold.
(For example, if we do not allow reduction under binders, then the eta
rule for functions won't hold (except perhaps in an
up-to-observability sort of way)).

--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe