TypeLits

[Richard Eisenberg]

Hi Iavor,

It was very nice to see you last week -- it's too bad we have to wait another year for another ICFP! :)

A question I got asked between sessions at ICFP led me to look at singletons again, and it seems that singletons has gone out of sync with TypeLits. When I looked closely at TypeLits, I saw a number of changes there, and I wonder if we can think a bit about the design before 7.8 rolls out. Forgive me if some of these suggestions are not new -- I just haven't looked closely at TypeLits for some time.

Specifically:

- I see that you define singleton instances for Bool. This makes sense, if we are to avoid orphan instances of the various singletons classes. But, it would seem helpful to define singleton support for more than just Bool here, if we are going down this road. For example, singletons for [], Maybe, Either, and the tuples are quite useful.

- You don't export the constructors for Sing (k :: Bool). I think these need to be publicly visible.

- I believe that Edward's reflection package will be incorporated into base. (Edward?) If so, it's possible that incoherentForgetSing can be cleaned up somewhat.

- Why use LocalProxy? What's wrong with plain old Proxy?

- I see Show and Read instances defined for singletons. Though these are useful, they prevent clients from defining their own instances, and I can imagine a user (possibly me) wanting a singleton to have a distinct Show instance from its base type. Perhaps these should be moved to a different module which can selectively be imported?

- The definition for (:~:) is redundant with the new Data.Type.Equality.

- The eqSing... functions are now redundant with the EqualityT class in Data.Type.Equality. Instead, TypeLits should probably define instances for EqualityT.

- TypeLits defines KindIs, which is redundant with Data.Proxy's KProxy. It might be that KindIs is easier to use than KProxy, but base probably shouldn't have both types floating around.

- I'm confused about IsZero. How is it different (in practical usage situations) from eqSingNat? Also, I'd like to note that IsZero uses a unary representation, which might be problematic.

- The definitions for Nat1 don't need to be in base. Perhaps we want them there -- I think it will get a lot of use -- but maybe we should just think about it for a moment before going forward.


I should admit that the redundancies are new -- after some discussion in the spring, I finally implemented the new bits that are now redundant with TypeLits only a month or two ago.

---

Now having posed these questions, here are my proposed answers:

- To avoid orphans, TypeLits should define singleton instances for all the types above, with all constructors exported.
- Remove redundancy with other parts of base. I personally prefer KProxy over KindIs, because I find the KindIs name confusing.
- Remove Show instances for singletons from base. If someone thinks these will have wide use, they can be defined in a library.
- Keep Nat1 right where it is.

Thoughts, anyone?

Thanks,
Richard