RFC: Singleton equality witnesses

[Iavor Diatchki]

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>
 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 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>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/20130212/48f1c744/attachment.htm>