TypeLits

[Iavor Diatchki]

Hello,

With the solver in GHC and the new closed type families you could write
something like this:

type family ToPeano (n :: Nat) where
  ToPeano 0 = Z
  ToPeano n = S (ToPeano (n-1))

The usual caveats about injectivity of type functions apply though, and for
larger numbers things may get slow when using unary.

-Iavor




On Sun, Oct 6, 2013 at 10:50 AM, Carter Schonwald <
carter.schonwald at gmail.com> wrote:

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