RFC: Singleton equality witnesses

Iavor Diatchki iavor.diatchki at gmail.com
Tue Feb 12 23:48:45 CET 2013

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

Here are some more detailed comments:

On Mon, Feb 11, 2013 at 6:40 PM, Richard Eisenberg <eir at cis.upenn.edu>

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


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>

More information about the ghc-devs mailing list