RFC: Singleton equality witnesses

Wed Feb 13 00:00:34 CET 2013

On 2/12/13, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> I've just pushed a commit to the type-reasoning branch with a strawman
> proposal of a reorganization of these definitions. Specifically, this commit
> breaks TypeLits into the following five files:
>
> - GHC.TypeEq, which contains the definitions for (:~:), Void, Refuted, etc.
> - GHC.Singletons, which contains the definitions about singletons in
> general, such as SingI and SingEquality
> - GHC.TypeLits.Unsafe, which contains just unsafeSingNat and
> unsafeSingSymbol
> - GHC.TypeLits.Internals, which is necessary to get GHC.TypeLits.Unsafe to
> have access to the right internals;
> this module is not exported from the 'base' package
> and
> - GHC.TypeLits, which contains the definitions specific to type-level
> literals.

As Simon said, having GHC.TypeLits.Unsafe and GHC.TypeLits.Internals
sounds like overkill, but it is similar to the other "unsafe"
functionality's whereabouts.
If we had an "export towards" feature then this division would make
perfect sense and users could only ever include GHC.TypeLits.Unsafe,
which should make their alarm bells ring. As I understand nobody
should include GHC.TypeLits.Internals (other than
GHC.TypeLits.Unsafe), but we cannot enforce that now. In light of this
I think it is okay to have two modules.

>
> Some thoughts on this design:
> - First off, why is TypeEq part of GHC?? Because we wish to write eqSingNat
> and eqSingSym in GHC.TypeLits, and that module rightly deserves to be part
> of GHC. I'm quite uncomfortable with this decision, and I even created a new
> git repo at github.com/goldfirere/type-reasoning to hold the definitions
> that eventually ended up in GHC.TypeEq. (The repo has nothing in it, now.)
> Perhaps the best resolution is to move eqSingNat and eqSingSym out of
> GHC.TypeLits and into an external package, but that seems silly in a
> different direction. (It is fully technically feasible, as those functions
> don't depend on any internals.) I would love some feedback here.

But doesn't the GHC type system need some inside knowledge of the Nat
and Symbol kinds?

> - Why is Singletons broken off? No strong reason here, but it seemed that
> the singletons-oriented definitions weren't solely related to type-level
> literals, so it seemed more natural this way.

I can understand this.

> - Making the Unsafe module was a little more principled, because those
> functions really are unsafe! They are quite useful, though, and should be
> available somewhere.
> - Currently, the internals of GHC assign types like "0" the kind
> GHC.TypeLits.Nat, so Nat and Symbol *must* remain in the GHC.TypeLits
> module. Unfortunately, the plumbing around GHC.TypeLits.Unsafe want Nat and
> Symbol to be defined in GHC.TypeLits.Internals. So, I created a
> TypeLits.hs-boot file to fix the problem. This is highly unsatisfactory, and
> if something like what I've done here sticks around, we should change the
> internals of GHC to use GHC.TypeLits.Internals.Nat, getting rid of the
> import cycle.
> - I've put in the decideSing function as discussed further up in this
> thread. Its implementation for Nat and Symbol must use unsafeCoerce, but
> that shouldn't be a surprise.

Great, hope to have a look at them soon.

>
> Unfortunately, the code doesn't compile now. This is because it needs SingI
> instances for, say, Sing 0. For a reason I have not explored, these
> instances are not available here, though they seem to be for code written
> outside of GHC. Iavor, any thoughts on this?
>
> Please tear any of these ideas (or my whole commit) to shreds! It really is
> meant to be a strawman proposal, but committing these changes seemed the
> best way of communicating on possible set of design decisions.

One thing i think is pretty much important, that I haven't seen
spelled out yet, is the "derive SingEquality" feature that can
probably be stacked upon all of this. After all, the decidable
equality should be rather mechanically derivable from any singleton
definition.

So overall, I like what I read here, of course the compilability
should be restored, but I cannot contribute at that end.

Thanks for the hard work, and cheers,

    Gabor

>
> Richard
>
> PS: I'm pasting much of this email to the wiki page for posterity.
>
> On Feb 7, 2013, at 10:45 AM, Iavor Diatchki <iavor.diatchki at gmail.com>
> wrote:
>
>> Hello,
>>
>> my preference would be to build this kind of functionality (and other
>> related features) in libraries on top of GHC.TypeLits.  This modules was
>> intended to contain only a minimal set of the constants that the compiler
>> needs to know about, and it already may have too much in it.
>>
>> On the concrete issue:  orphan instances could be avoided if the type lits
>> instances are defined in the same module as the class.
>>
>> -Iavor
>>
>>
>> On Thu, Feb 7, 2013 at 6:50 AM, Gabor Greif <ggreif at gmail.com> wrote:
>> In its current state it is not tied to TypeLits, but when Richard adds
>> his magic it probably will be. It is still an open issue where to put
>> what, and whether a new module would be fitting.
>> Richard surely will comment on this. I'd prefer the new instance
>> definitions in TypeLits to avoid orphans. Thanks for your input
>> though, this is exactly the kind of feedback we were hoping for :-)
>>
>> Cheers,
>>
>>     Gabor
>>
>>
>> [looks like I lost a previous version of this response, sorry if you
>> get it twice]
>>
>> On 2/7/13, José Pedro Magalhães <jpm at cs.uu.nl> wrote:
>> > Hey Gabor,
>> >
>> > And why should it be part of base? Don't get me wrong, I'm not saying
>> > this
>> > is not important/useful. I'm just wondering about the reason to have it
>> > in
>> > base.
>> > Is it tied to TypeLits?
>> >
>> >
>> > Cheers,
>> > Pedro
>> >
>> > On Thu, Feb 7, 2013 at 2:21 PM, Gabor Greif <ggreif at gmail.com> wrote:
>> >
>> >> Oi José,
>> >>
>> >> this is a library-only issue, the branch is in libraries/base, thus
>> >> somewhat tied to the 7.8 release.
>> >>
>> >> Cheers,
>> >>
>> >>     Gabor
>> >>
>> >> On 2/7/13, José Pedro Magalhães <jpm at cs.uu.nl> wrote:
>> >> > On Wed, Feb 6, 2013 at 7:17 PM, Gabor Greif <ggreif at gmail.com>
>> >> > wrote:
>> >> >
>> >> >> On 2/6/13, Richard Eisenberg <eir at cis.upenn.edu> wrote:
>> >> >> > The only thing that stops me from saying "push" is that I think
>> >> >> > there
>> >> >> > is
>> >> >> a
>> >> >> > better organization for all of this. The ideas we're discussing
>> >> >> > here
>> >> >> (things
>> >> >> > like the Void type) don't seem to belong in TypeLits -- it has
>> >> >> > nothing
>> >> >> to do
>> >> >> > with literals. Time for a GHC.TypeReasoning module? Does someone
>> >> >> > have
>> >> a
>> >> >> > better name?
>> >> >>
>> >> >> Sounds okay. We can wiggle around on the new branch 'till we feel
>> >> >> comfortable, but I'd like to land this on master before the v7.8
>> >> >> train
>> >> >> leaves the station (i.e. the release branch is created).
>> >> >>
>> >> >
>> >> > Can you perhaps summarise exactly what needs to be added to GHC for
>> >> > this
>> >> to
>> >> > work?
>> >> > It's not immediately clear to me why this is not just a library
>> >> > issue.
>> >> >
>> >> >
>> >> > Thanks,
>> >> > Pedro
>> >> >
>> >>
>> >
>>
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://www.haskell.org/mailman/listinfo/ghc-devs
>>
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://www.haskell.org/mailman/listinfo/ghc-devs
>
>