RFC: Singleton equality witnesses
iavor.diatchki at gmail.com
Tue Feb 12 23:48:45 CET 2013
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
> - 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
> - GHC.TypeLits, which contains the definitions specific to type-level
> 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
> ** **
> ** **
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the ghc-devs