TypeLits

[Carter Schonwald]

hrmm, Why don't we have a proper bijection?

lets assume we have ToPeano and a corresponding ToNat, as above,

couldn't we have something like

asPeano :: (b~ ToPeano a, a ~ ToNat b)=> Proxy a -> Proxy b

or a suitable type level representaion thereof?

or are you saying that in 7.8, i should be able to just efficiently work
directly on the nat rep

and have

class Cl (n::Nat) where

instance CL 0 where

instance Cl n => Cl (n+1)

and essentially get peano for free?


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

> 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/2955c67e/attachment.html>