TypeLits

[Edward Kmett]

I've been talking to Austin about GHC.Reflection.

He'd expressed some interest in taking a whack at it. If he doesn't get to
it before this weekend, then I will.

Re Proxy, we now have Proxy# as well.

-Edward




On Mon, Sep 30, 2013 at 11:58 PM, Richard Eisenberg <eir at cis.upenn.edu>wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20131001/5be21410/attachment.html>