TypeLits

[Iavor Diatchki]

Hello,

a lot of the complexity in GHC.TypeLits was added to support the
`singletons` package, but since the two apparently diverged, I simplified
GHC.TypeLits so that it is back to providing just the basics.  As we
discussed, the more general singletons framework should probably be in
`singletons`.  So, to summarize, these are the functions exposed from
GHC.TypeLits at the moment:

natVal        :: KnownNat n    => Proxy n -> Integer
symbolVal     :: KnownSymbol n => Proxy n -> String

someNatVal    :: Integer -> Maybe SomeNat
someSymbolVal :: String  ->       SomeSymbol

data SomeNat     = forall n. KnownNat n    => SomeNat    (Proxy n)
data SomeSymbol  = forall n. KnownSymbol n => SomeSymbol (Proxy n)

The classes `KnownNat` and `KnownSymbol` have instances for concrete
type-level literals of kind `Nat` and `Symbol` respectively.

-Iavor

PS:  A lot of the duplication in GHC.TypeLits  was there because it was
implemented before some of the other libraries appeared in base (e.g.,
Data.Proxy and Data.Type.Equality).  I didn't know about these and, I
guess, whoever added them didn't know about GHC.TypeLits so it never got
updated.







On Tue, Oct 1, 2013 at 10:49 AM, Edward Kmett <ekmett at gmail.com> wrote:

> 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/20131006/a5a67b89/attachment-0001.html>