[Haskell-cafe] 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" <eir at cis.upenn.edu> 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> 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
Haskell-Cafe at haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160411/57bca360/attachment.html>