RFC: Singleton equality witnesses

[Simon Peyton-Jones]

Thanks for pushing on this!   The summary of my comments is this:  I think that we should have 1 or 2 low-level (not necessarily safe) GHC modules that contain all the bits that GHC needs to know about, and move all other bits into a separate library, which is to be used by the actual users of the system.  In this way, this library could evolve independently of GHC releases.

That makes sense to me.  Perhaps the bits that *are* in GHC.XX can be commented to say *why* they are?  Eg SingI needs to be there because GHC know about the singleton instances for type level literals. etc.

Simon

From: Iavor Diatchki [mailto:iavor.diatchki at gmail.com]
Sent: 12 February 2013 22:49
To: Simon Peyton-Jones
Cc: Richard Eisenberg; José Pedro Magalhães; ghc-devs
Subject: Re: RFC: Singleton equality witnesses

Hi Richard,

Thanks for pushing on this!   The summary of my comments is this:  I think that we should have 1 or 2 low-level (not necessarily safe) GHC modules that contain all the bits that GHC needs to know about, and move all other bits into a separate library, which is to be used by the actual users of the system.  In this way, this library could evolve independently of GHC releases.

Here are some more detailed comments:

On Mon, Feb 11, 2013 at 6:40 PM, Richard Eisenberg <eir at cis.upenn.edu<mailto: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.

Like Simon, I think that there is no need to distinguish between TypeList.Unsafe and TypeLits.Internals.

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<http://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.

We could move these out of GHC: they are just defined using (a safe use of) `unsafeCoerce`.  They just need to know about the equality type (:~:), so I think they should be defined wherever the equality type is defined.

Also, an unrelated piece of advice:  try to keep down the use of type synonyms---they make libraries seem complex.  For example, most programmers would understand the type 'a -> Void', but when I see `Refuted a` I have to go lookup its definition and check if there is something special about it.

- 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 don't think this matters too much either way, but I would look for things to remove from here and move to the programmer facing library.  For example, why should `SingEquality` be there?  It is important for `SingI` to be in GHC, because the instances for type-level literals are wired into GHC: it expects the class to be in GHC.TypeLits (this is why moving the class broke the instances, take a look in `compiler/prelude/TysWiredIn.lhs`, indeed, `Nat` and `Symbol` are also wired into GHC in the same module).

- 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.

Yes, I think that we want to export these at least for the use by the programmer facing library---it may choose not to re-export them.

-Iavor


On Tue, Feb 12, 2013 at 12:38 AM, Simon Peyton-Jones <simonpj at microsoft.com<mailto:simonpj at microsoft.com>> wrote:
- 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.

Let’s NOT have an hs-boot file here.  Instead, change PrelNames to tell GHC where Nat and Symbol are defined.  It’s ok for them to be in Internals.

I’m also unconvinced about the distinction between “Internals” and “Unsafe”.  To me the former connotes the latter.  Import Internals if you know what you are doing; eg that might let you break important invariants.  Import a kosher module like TypeLits if you want the Joe Programmer interface.

Simon



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130213/0af02cbb/attachment-0001.htm>