TypeLits

Sun Oct 6 17:50:30 UTC 2013

relatedly: to what extent are we planning/are able to support being able to
map between a type Nats as they're exposed in TypeLits currently, and a
Peano view?

That is: Why don't we have a way to map between Nat and PeanoNat, where
PeanoNat could be a datakinds type like so
data PeanoNat = S !PeanoNat | Z
or something of that sort?

Or equivalently, provide that destructuring/constructing facility directly
on the Nat type itself!

Does the solver machinery in 7.8 give us that sort of facility for free? Is
it expressible without any GHC side work? Or *must* it be on GHC side
support wise?

I'm asking because i have a use case where I'd love to have the type Nats
syntax, but also be able to define my instances over Nats in the Peano style

thanks
-Carter

On Sun, Oct 6, 2013 at 1:07 PM, Iavor Diatchki <iavor.diatchki at gmail.com>wrote:

> 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
>>>
>>
>>
>
> _______________________________________________
> 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/9c31c4a3/attachment.html>