Hello, I have updated `GHC.TypeLits` to avoid the use of `Any` and also to use type families instead of functional dependencies. The new version should be in `base` on the `master` branch. I described the basic idea of what I did on this wiki page:
http://hackage.haskell.org/trac/ghc/wiki/TypeNats/SingletonsAndKinds As usual, feedback is most welcome. -Iavor On Mon, Oct 15, 2012 at 6:13 PM, Richard Eisenberg <e...@cis.upenn.edu>wrote: > I think there's a decent record of this conversation at > http://hackage.haskell.org/trac/ghc/ticket/7259 > > The comments there skip over some of the discussion in this thread, but I > think the key ideas are all there. > > Here is how I see things: > - Yes, I believe Any can be turned back into a type family, and Iavor and > I will refactor around this change. As for my singletons paper, this > changes the encoding slightly, but nothing major. I think it's a change for > the better in the long run. > - I raised a concern about type inference in the presence of eta-expansion > in an earlier post to this thread and on the Trac page. Before really > moving forward here, I think it would good for others to think about these > issues. Instead of rehashing the idea again, please do visit the Trac page > and comment there. > - At one point, this thread included a discussion of injective type > families. While these would be a nice thing to have, they seem orthogonal > at this point and are probably best dropped from this discussion (which > seems to have happened naturally, at any rate). > > Richard > > On Oct 15, 2012, at 8:10 PM, Simon Peyton-Jones <simo...@microsoft.com> > wrote: > > I’m afraid I’ve rather lost track of this thread. Would someone care to > summarise, on a wiki page perhaps? **** > > I think the story is:**** > > · Inspired by Nick’s idea, Iavor and Pedro have converged on a > single, type-family-based style for defining singletons.**** > · This style no longer requires Any to be a data type, so I can > turn it back into a type family, which is a Good Thing because it paves the > way for an eta rule. RSVP and I’ll do that.**** > · Iavor mutters about sketchiness, but I’m not sure what that > means specifically. **** > · I’m not sure how, it at all, it affects Richard’s singletons > paper**** > > Simon**** > > > *From:* Iavor Diatchki [mailto:diatc...@galois.com] > *Sent:* 12 October 2012 21:11 > *To:* Richard Eisenberg > *Cc:* Nicolas Frisby; Simon Peyton-Jones; Stephanie Weirich; Conor > McBride; glasgow-haskell-users@haskell.org > *Subject:* Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a > functional dependency?**** > ** ** > Hello, > > (summary: I think Nick's idea works for what's in GHC.TypeLits, and it > would allow us to switch from `Any` as a constructor to `Any` as a > function.) > > On 10/11/2012 08:47 PM, Richard Eisenberg wrote:**** > > Iavor and I collaborated on the design of the building blocks of singleton > types, as we wanted our work to be interoperable. A recent scan through > TypeLits tells me, though, that somewhere along the way, our designs > diverged a bit. Somewhere on the to-do list is to re-unify the interfaces, > and actually just to import TypeLits into Data.Singletons so the > definitions are one and the same. Iavor, I'm happy to talk about the > details if you are.**** > > > The module GHC.TypeLits hasn't really changed much since last we talked > (the Nat1 type is new, but that's only for working with type-level naturals > and unrelated to this discussion). I added the SingE class so that my work > is compatible with Richard's (a simple newtype suffices if we are only > interested in working with singletons for type-level literals). So we > should certainly make the two compatible again, let me know what needs to > change. > > I was just playing around with Nick's idea and here is my version of the > code, which loads fine (but as I discuss in point 2 bellow I think it is a > bit sketchy...) > > import GHC.TypeLits hiding (SingE(..), Kind) > import qualified GHC.TypeLits as Old > > data Kind (k :: *) -- discuessed in point 2 bellow > > class SingE (any :: Kind k) rep | any -> rep where > fromSing :: Sing (a :: k) -> rep > > instance SingE (any :: Kind Nat) Integer where > fromSing = Old.fromSing > > instance SingE (any :: Kind Symbol) String where > fromSing = Old.fromSing > > I think that there are two interesting points about this code: > > 1. It is important that the instances are polymorphic because this tells > GHC that it is allowed to use the instance in any context as long as the > kinds match, regardless of the actual type. Note that this is not > the case if we write the instance using the singleton member of the proxy > kind: > > **** > > data KindProxy (k :: *) = KindProxy**** > > ** ** > > instance SingE ('KindProxy :: KindProxy Nat) Integer where**** > > fromSing (SNat n) = n**** > > Such instances would only work if GHC could see that the type is > 'KindProxy so if we have a type variable of the correct kind, the > instance would not reduce. This is related to the eta-expansion > issue---if we eliminated `Any`, then GHC could perform a kind-based > improvement to deduce that the type variable must be equal to `KindProxy`, > because this is the only type with the correct kind. > > > 2. As Nick noticed, we are not doing any fancy type computing in the > class, so we don't actually need any KindProxy elements---we are just doing > overloading based on a kind rather than a type. To emphasize this I made > Kind an empty type/kind and GHC is still happy: instances are resolved as > intended. But... `Kind` has no elements so what are the instances applied > to? The only reason this works is that GHC has defaulted the instances to > use `Any`. To me this seems a bit sketchy. > > > > So what to do? Changing the code in this style (using the normal > non-empty proxy) makes sense because I think that it would allow us to > change `Any` into a type function rather than a type constructor, like > Simon did and un-did recently. The reason I think this will work is > because now there will be no uses of `Any` in the definitions of the > instances, it will only appear in the uses of the instances. > > Furthermore, I think it makes sense for GHC to check that for each use of > the type function `Any`, the kind where it is used is non-empty. I'm not > sure how easy it would be to implement that, so maybe we can deal with it > later. > > -Iavor > > > > _______________________________________________ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
