<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"><base href="x-msg://370/"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div>I think there's a decent record of this conversation at <a href="http://hackage.haskell.org/trac/ghc/ticket/7259">http://hackage.haskell.org/trac/ghc/ticket/7259</a></div><div><br></div><div>The comments there skip over some of the discussion in this thread, but I think the key ideas are all there.</div><div><br></div><div>Here is how I see things:</div><div>- 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.</div><div>- 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.</div><div>- 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).</div><div><br></div><div>Richard</div><br><div><div>On Oct 15, 2012, at 8:10 PM, Simon Peyton-Jones <<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div bgcolor="white" lang="EN-GB" link="blue" vlink="purple" style="font-family: Helvetica; font-size: medium; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: -webkit-auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; "><div class="WordSection1" style="page: WordSection1; "><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "><span style="font-size: 11pt; font-family: Verdana, sans-serif; color: rgb(31, 73, 125); ">I’m afraid I’ve rather lost track of this thread. Would someone care to summarise, on a wiki page perhaps? <o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "><span style="font-size: 11pt; font-family: Verdana, sans-serif; color: rgb(31, 73, 125); "> <br>I think the story is:<o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "><span style="font-size: 11pt; font-family: Verdana, sans-serif; color: rgb(31, 73, 125); "> </span></div><div style="margin: 0cm 0cm 0.0001pt 36pt; font-size: 12pt; font-family: 'Times New Roman', serif; text-indent: -18pt; "><span style="font-size: 11pt; font-family: Symbol; color: rgb(31, 73, 125); "><span>·<span style="font-style: normal; font-variant: normal; font-weight: normal; font-size: 7pt; line-height: normal; font-family: 'Times New Roman'; "> <span class="Apple-converted-space"> </span></span></span></span><span style="font-size: 11pt; font-family: Verdana, sans-serif; color: rgb(31, 73, 125); ">Inspired by Nick’s idea, Iavor and Pedro have converged on a single, type-family-based style for defining singletons.<o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt 36pt; font-size: 12pt; font-family: 'Times New Roman', serif; text-indent: -18pt; "><span style="font-size: 11pt; font-family: Symbol; color: rgb(31, 73, 125); "><span>·<span style="font-style: normal; font-variant: normal; font-weight: normal; font-size: 7pt; line-height: normal; font-family: 'Times New Roman'; "> <span class="Apple-converted-space"> </span></span></span></span><span style="font-size: 11pt; font-family: Verdana, sans-serif; color: rgb(31, 73, 125); ">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.<o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt 36pt; font-size: 12pt; font-family: 'Times New Roman', serif; text-indent: -18pt; "><span style="font-size: 11pt; font-family: Symbol; color: rgb(31, 73, 125); "><span>·<span style="font-style: normal; font-variant: normal; font-weight: normal; font-size: 7pt; line-height: normal; font-family: 'Times New Roman'; "> <span class="Apple-converted-space"> </span></span></span></span><span style="font-size: 11pt; font-family: Verdana, sans-serif; color: rgb(31, 73, 125); ">Iavor mutters about sketchiness, but I’m not sure what that means specifically. <o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt 36pt; font-size: 12pt; font-family: 'Times New Roman', serif; text-indent: -18pt; "><span style="font-size: 11pt; font-family: Symbol; color: rgb(31, 73, 125); "><span>·<span style="font-style: normal; font-variant: normal; font-weight: normal; font-size: 7pt; line-height: normal; font-family: 'Times New Roman'; "> <span class="Apple-converted-space"> </span></span></span></span><span style="font-size: 11pt; font-family: Verdana, sans-serif; color: rgb(31, 73, 125); ">I’m not sure how, it at all, it affects Richard’s singletons paper<o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "><span style="font-size: 11pt; font-family: Verdana, sans-serif; color: rgb(31, 73, 125); "> </span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "><span style="font-size: 11pt; font-family: Verdana, sans-serif; color: rgb(31, 73, 125); ">Simon<o:p></o:p></span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "><span style="font-size: 11pt; font-family: Verdana, sans-serif; color: rgb(31, 73, 125); "> </span></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "><span style="font-size: 11pt; font-family: Verdana, sans-serif; color: rgb(31, 73, 125); "> </span></div><div style="border-style: none none none solid; border-left-width: 1.5pt; border-left-color: blue; padding: 0cm 0cm 0cm 4pt; "><div><div style="border-style: solid none none; border-top-width: 1pt; border-top-color: rgb(181, 196, 223); padding: 3pt 0cm 0cm; "><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "><b><span lang="EN-US" style="font-size: 10pt; font-family: Tahoma, sans-serif; color: windowtext; ">From:</span></b><span lang="EN-US" style="font-size: 10pt; font-family: Tahoma, sans-serif; color: windowtext; "><span class="Apple-converted-space"> </span>Iavor Diatchki [mailto:diatchki@<a href="http://galois.com">galois.com</a>]<span class="Apple-converted-space"> </span><br><b>Sent:</b><span class="Apple-converted-space"> </span>12 October 2012 21:11<br><b>To:</b><span class="Apple-converted-space"> </span>Richard Eisenberg<br><b>Cc:</b><span class="Apple-converted-space"> </span>Nicolas Frisby; Simon Peyton-Jones; Stephanie Weirich; Conor McBride; <a href="mailto:glasgow-haskell-users@haskell.org">glasgow-haskell-users@haskell.org</a><br><b>Subject:</b><span class="Apple-converted-space"> </span>Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?<o:p></o:p></span></div></div></div><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "><o:p> </o:p></div><div><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; ">Hello,<br><br>(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.)<br><br>On 10/11/2012 08:47 PM, Richard Eisenberg wrote:<o:p></o:p></div></div><blockquote style="margin-top: 5pt; margin-bottom: 5pt; "><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; ">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.<o:p></o:p></div></blockquote><div style="margin: 0cm 0cm 0.0001pt; font-size: 12pt; font-family: 'Times New Roman', serif; "><br>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.<br><br>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...)<br><br><span style="font-family: 'Courier New'; ">import GHC.TypeLits hiding (SingE(..), Kind)<br>import qualified GHC.TypeLits as Old<br><br>data Kind (k :: *) -- discuessed in point 2 bellow<br><br>class SingE (any :: Kind k) rep | any -> rep where<br> fromSing :: Sing (a :: k) -> rep<br><br>instance SingE (any :: Kind Nat) Integer where<br> fromSing = Old.fromSing<br><br>instance SingE (any :: Kind Symbol) String where<br> fromSing = Old.fromSing<br></span><br>I think that there are two interesting points about this code:<br><br>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<span class="Apple-converted-space"> </span><br>the case if we write the instance using the singleton member of the proxy kind:<br><br><o:p></o:p></div><pre style="margin: 0cm 0cm 0.0001pt; font-size: 10pt; font-family: 'Courier New'; ">data KindProxy (k :: *) = KindProxy<o:p></o:p></pre><pre style="margin: 0cm 0cm 0.0001pt; font-size: 10pt; font-family: 'Courier New'; "><o:p> </o:p></pre><pre style="margin: 0cm 0cm 0.0001pt; font-size: 10pt; font-family: 'Courier New'; ">instance SingE ('KindProxy :: KindProxy Nat) Integer where<o:p></o:p></pre><pre style="margin: 0cm 0cm 0.0001pt; font-size: 10pt; font-family: 'Courier New'; "> fromSing (SNat n) = n<o:p></o:p></pre><p class="MsoNormal" style="margin: 0cm 0cm 12pt; font-size: 12pt; font-family: 'Times New Roman', serif; ">Such instances would only work if GHC could see that the type is<span class="Apple-converted-space"> </span><span style="font-family: 'Courier New'; ">'KindProxy</span><span class="Apple-converted-space"> </span>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. <span class="Apple-converted-space"> </span><br><br><br>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<span style="font-family: 'Courier New'; ">Kind</span><span class="Apple-converted-space"> </span>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.<br><br><br>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.<br><br>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.<br><br>-Iavor</p></div></div></div></blockquote></div><br></body></html>