PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

[Iavor Diatchki]

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 <eir at 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 <simonpj at 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:diatchki at galois.com]
> *Sent:* 12 October 2012 21:11
> *To:* Richard Eisenberg
> *Cc:* Nicolas Frisby; Simon Peyton-Jones; Stephanie Weirich; Conor
> McBride; glasgow-haskell-users at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20121015/94810364/attachment.htm>