TypeLits

[Simon Peyton-Jones]

Great post. It would be very good to clear this up asap, ie before 7.8, which itself is imminent.  I'm agnostic about all of this ... from my pov just go ahead!

Simon

| -----Original Message-----
| From: Libraries [mailto:libraries-bounces at haskell.org] On Behalf Of
| Richard Eisenberg
| Sent: 01 October 2013 04:59
| To: Iavor Diatchki
| Cc: libraries Libraries
| Subject: TypeLits
| 
| 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
| _______________________________________________
| Libraries mailing list
| Libraries at haskell.org
| http://www.haskell.org/mailman/listinfo/libraries