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 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 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 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@haskell.org http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

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 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@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 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 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 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@haskell.org http://www.haskell.org/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

hey Iavor, I just tried out today's head on a slightly more interesting example, and i hit the limits of the type nat solver, http://ghc.haskell.org/trac/ghc/ticket/8422#comment:1 it seems like something where the solver *should* work On Mon, Oct 7, 2013 at 1:35 AM, Iavor Diatchki wrote:

Hi,

On Sun, Oct 6, 2013 at 4:36 PM, Carter Schonwald < carter.schonwald@gmail.com> wrote:

...

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?

I think it should be quite easy to define such a function, but I am afraid I don't fully understand how to use it...

...

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?

...

...

...

...

> I am not sure if this would help with your specific task, but things like this work:

{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-} {-# LANGUAGE FlexibleInstances, UndecidableInstances, OverlappingInstances #-} import GHC.TypeLits import Data.Proxy

class C (n :: Nat) where txt :: Proxy n -> String

instance C 0 where txt _ = "0"

instance C (n - 1) => C n where txt x = "1 + " ++ txt (prev x)

prev :: Proxy x -> Proxy (x - 1) prev _ = Proxy

example = txt (Proxy :: Proxy 3)

*Main> example "1 + 1 + 1 + 0"

-Iavor PS: All of this is committed in HEAD, please try it out and let me know if we need to do any last minute changes before the upcoming release.

gotcha what are the technical obstacles to getting solver for at least Presburger Arithmetic in? I'd be willing to even do the footwork if there was any shadow of a chance of geting that into 7.8 as a *bugfix* (or failing that, helping kick it along post 7.8, but i've enough other contribs planned post 7.8 release) cheers -Carter On Tue, Oct 8, 2013 at 7:49 PM, Iavor Diatchki wrote:

Hi,

yeah, I know :-) The current solver can only evaluate concrete things, for example it knows that 5 + 3 ~ 8, but it can't do any abstract reasoning (i.e., when there are variables around). So things like GADTs pretty much don't work at the moment.

-Iavor

On Tue, Oct 8, 2013 at 2:08 PM, Carter Schonwald < carter.schonwald@gmail.com> wrote:

...

hey Iavor, I just tried out today's head on a slightly more interesting example, and i hit the limits of the type nat solver,

http://ghc.haskell.org/trac/ghc/ticket/8422#comment:1

it seems like something where the solver *should* work

On Mon, Oct 7, 2013 at 1:35 AM, Iavor Diatchki wrote:

...

Hi,

On Sun, Oct 6, 2013 at 4:36 PM, Carter Schonwald < carter.schonwald@gmail.com> wrote:

...

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?

I think it should be quite easy to define such a function, but I am afraid I don't fully understand how to use it...

...

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?

...

...

>>> I am not sure if this would help with your specific task, but things like this work:

{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-} {-# LANGUAGE FlexibleInstances, UndecidableInstances, OverlappingInstances #-} import GHC.TypeLits import Data.Proxy

class C (n :: Nat) where txt :: Proxy n -> String

instance C 0 where txt _ = "0"

instance C (n - 1) => C n where txt x = "1 + " ++ txt (prev x)

prev :: Proxy x -> Proxy (x - 1) prev _ = Proxy

example = txt (Proxy :: Proxy 3)

*Main> example "1 + 1 + 1 + 0"

-Iavor PS: All of this is committed in HEAD, please try it out and let me know if we need to do any last minute changes before the upcoming release.