GHC: Ticket #8778: Typeable TypeNats
http://ghc.haskell.org/trac/ghc/ticket/8778
<p>
It would be useful (the case I have at hand is for some scenarios involving checking of physical dimensions) to be able to combine the Data.Dynamic story with the GHC.TypeLits story.
</p>
<p>
A Typeable instance for every Nat is the sticking point.
</p>
<p>
(I do not know if this is even theoretically possible.)
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/8778
Trac 1.0.1BjornBuckwalterThu, 13 Feb 2014 08:37:11 GMTcc set
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:1
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:1
<ul>
<li><strong>cc</strong>
<em>bjorn.buckwalter@…</em> added
</li>
</ul>
TicketcarterThu, 13 Feb 2014 09:00:16 GMT
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:2
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:2
<p>
@dmcclean could you please explain what you mean? Make up some pseudo code please!
</p>
<p>
Are you thinking about type level existentials?
</p>
TicketthoughtpoliceThu, 13 Feb 2014 13:52:37 GMTversion deleted
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:3
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:3
<ul>
<li><strong>version</strong>
<em>7.8.1-rc1</em> deleted
</li>
</ul>
<p>
This isn't going to happen in time for 7.8.1.
</p>
TicketdmccleanThu, 13 Feb 2014 16:25:48 GMTattachment set
http://ghc.haskell.org/trac/ghc/ticket/8778
http://ghc.haskell.org/trac/ghc/ticket/8778
<ul>
<li><strong>attachment</strong>
set to <em>Test8778.hs</em>
</li>
</ul>
<p>
Test case
</p>
TicketdmccleanThu, 13 Feb 2014 16:28:40 GMT
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:4
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:4
<p>
Sorry about that, thoughtpolice, I was thinking the field was for where I saw it.
</p>
<p>
Example (also attached, but here for discussion):
</p>
<pre class="wiki">{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE AutoDeriveTypeable #-}
module Test8778 where
import GHC.TypeLits
import Data.Dynamic
data Phantom (n :: Nat) = Phantom
desirable = toDyn (Phantom :: Phantom 3)
</pre><p>
Results in:
</p>
<pre class="wiki"> No instance for (Typeable 3) arising from a use of `toDyn'
In the expression: toDyn (Phantom :: Phantom 3)
In an equation for `desirable':
desirable = toDyn (Phantom :: Phantom 3)
Failed, modules loaded: none.
</pre><p>
This is unfortunate because it means that you can't use Data.Dynamic with any types that have phantom Nat parameters. Up a couple of levels in the abstraction hierarchy, this makes it difficult to build a user interface that works well with displaying signals and taking input of arbitrary dimensional types (lengths, velocities, currents, and the like).
</p>
TicketthoughtpoliceThu, 13 Feb 2014 16:34:52 GMTversion set
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:5
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:5
<ul>
<li><strong>version</strong>
set to <em>7.8.1-rc1</em>
</li>
</ul>
<p>
Actually I was sort of reclassifying the tickets and that was my mistake to remove the version :) I've changed it back. And thank you for the example!
</p>
TicketdreixelThu, 13 Feb 2014 17:21:28 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:6
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:6
<ul>
<li><strong>cc</strong>
<em>iavor.diatchki@…</em> added
</li>
</ul>
<p>
Iavor has looked into this, so he might have some status update...
</p>
TicketcarlhowellsMon, 02 Jun 2014 17:07:25 GMT
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:7
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:7
<p>
If this is possible, it'd be really great to have. For Symbols, too. Just because sometimes Typeable is helpful, and for the times when it is, it's nice for new fancy types to be instances of it as well.
</p>
TicketcrockeeaWed, 11 Jun 2014 13:46:37 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:8
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:8
<ul>
<li><strong>cc</strong>
<em>ecrockett0@…</em> added
</li>
</ul>
TicketIavor S. Diatchki <iavor.diatchki@…>Sat, 14 Jun 2014 21:51:41 GMT
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:9
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:9
<p>
In <a class="changeset" href="http://ghc.haskell.org/trac/ghc/changeset/0354fb3676e5b0044601c8e0a5f8039f0cac0c8d/ghc" title="Implement `Typeable` support for type-level literals (#8778).">0354fb3676e5b0044601c8e0a5f8039f0cac0c8d/ghc</a>:
</p>
<pre class="message">Implement `Typeable` support for type-level literals (#8778).</pre>
Ticketsjoerd_visscherSat, 14 Jun 2014 23:32:15 GMT
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:10
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:10
<p>
Should the performance fix from <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/9203" title="bug: Perf regression in 7.8.2 relative to 7.6.3, possibly related to HashMap (closed: fixed)">#9203</a> be applied here too?
</p>
TicketdiatchkiSun, 15 Jun 2014 00:49:58 GMT
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:11
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:11
<p>
I'd be happy to make whatever changes are needed, but could you summarize what I should do? The <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/9203" title="bug: Perf regression in 7.8.2 relative to 7.6.3, possibly related to HashMap (closed: fixed)">#9203</a> ticket just talks about HashMaps, and there is a link to Phabricator, but I don't have an account for that...
</p>
TicketsimonpjMon, 16 Jun 2014 08:10:15 GMT
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:12
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:12
<p>
The issue in <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/9203" title="bug: Perf regression in 7.8.2 relative to 7.6.3, possibly related to HashMap (closed: fixed)">#9203</a> is that a <tt>Typeable</tt> instance should look like
</p>
<pre class="wiki">instance Typeable ... where
typeRep# = \_ -> rep
where
rep = ...blah...
</pre><p>
and NOT like
</p>
<pre class="wiki">instance Typeable ... where
typeRep# p = ...blah...
</pre><p>
to ensure that the computation of <tt>rep</tt> is shared among all invocations of <tt>typeRep#</tt>.
</p>
<p>
So Sjoerd is quite right, I think.
</p>
<p>
(I'm a bit confused because I thought we only allowed machine-generated instances of <tt>Typeable</tt>.)
</p>
<p>
BTW if you have a Github account you automatically have a Phabricator account.
</p>
<p>
Simon
</p>
TicketIavor S. Diatchki <diatchki@…>Mon, 16 Jun 2014 22:59:24 GMT
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:13
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:13
<p>
In <a class="changeset" href="http://ghc.haskell.org/trac/ghc/changeset/836981c7dec5c794ca94408468535cc018dc2e82/ghc" title="Redo instance to be more efficient (see #8778, #9203)">836981c7dec5c794ca94408468535cc018dc2e82/ghc</a>:
</p>
<pre class="message">Redo instance to be more efficient (see #8778, #9203)</pre>
TicketdiatchkiMon, 16 Jun 2014 23:08:56 GMT
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:14
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:14
<p>
Aha, thanks for the Phabricator tip!
</p>
<p>
I redid the instances to be of the form <tt>\_ -> blah</tt>.
</p>
<p>
About the <tt>Typeable</tt> instance: in normal modules we only allow machine-generated instances. The module <tt>Data.Typeable.Internal</tt> is an exception though---it allows manual instances to accommodate custom instances for some types.
</p>
<p>
One note about the type-literal instances: they have a much higher chance of collision than a typical kind, as both <tt>Nat</tt> and <tt>Symbol</tt> have infinitely many type-constructors, which need to fit into the fingerprint. I am not sure how much of a realistic problem this is, but it is something to keep in mind.
</p>
TicketaavogtTue, 17 Jun 2014 02:32:10 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:15
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:15
<ul>
<li><strong>cc</strong>
<em>vogt.adam@…</em> added
</li>
</ul>
TicketsimonpjTue, 17 Jun 2014 08:28:48 GMT
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:16
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:16
<p>
Re your "note about type-literal instances": did you add a <tt>Note</tt> with the relevant code. it is 100x times more likely to come to someone's attention there than in this ticket!
</p>
<p>
Thanks
</p>
<p>
Simon
</p>
TicketdiatchkiTue, 17 Jun 2014 17:38:57 GMT
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:17
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:17
<p>
It occurred to me that we could work around the collision problem as follows: in the current representation I am representing each type-level number as its own type-constructor, leading to the collision problem as we need more type constructors than the 128-bit that we have.
</p>
<p>
An alternative would be to think of the numbers as non-empty lists of digits in some large base (e.g. 8192). In other words, we could generate the representation as if the numbers were defined like this:
</p>
<pre class="wiki">data Nat = Nil0 | Nil1 | Nil2 | ... | Nil8191
| Cons1 Nat | Cons2 Nat | ... | Cons8191 Nat
</pre><p>
Pros:
</p>
<ul><li>Potentially avoids the chance of collisions as now we need to represent only ~16000 constructors, rather than infinitely many.
</li><li>Reasonably sized numbers are represented just as efficiently, and very large numbers are only slightly less efficient.
</li></ul><p>
Cons:
</p>
<ul><li>A bit slower to compute representation?
</li><li>Functions like <tt>splitTyConApp</tt> would allow users to observe this encoding, although I am not sure that this matters?
</li></ul><p>
In the "Pros" list I say "potentially" because even though the <tt>TypeRep</tt> is a tree of type applications, when we compare for equality we are just comparing the fingerprint, so I am not sure that we've actually gained anything by all this...
</p>
<p>
Thoughts?
</p>
TicketdiatchkiTue, 17 Jun 2014 21:10:33 GMT
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:18
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:18
<p>
I looked some more at the code, and realized that this more complex encoding is not worth the effort: we are always hashing the entire type-representation, so it does not matter how the types are encoded. Also, it looks like we are using a reasonable hashing function (MD5), and collisions for it are very unlikely so we should be OK.
</p>
<p>
So, I guess we can close this ticket, unless there are any more issues?
</p>
TicketsimonpjWed, 18 Jun 2014 08:10:41 GMT
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:19
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:19
<p>
I agree. But still worth a <tt>Note</tt>!
</p>
<p>
Simon
</p>
TicketdmccleanWed, 18 Jun 2014 14:43:06 GMT
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:20
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:20
<p>
Thanks, Iavor!
</p>
TicketcrockeeaSun, 17 Aug 2014 19:18:39 GMT
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:21
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:21
<p>
What's the milestone for this patch?
</p>
TicketsimonpjSun, 17 Aug 2014 21:19:48 GMTowner set
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:22
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:22
<ul>
<li><strong>owner</strong>
set to <em>diatchki</em>
</li>
</ul>
<p>
crokeea: I think it's done already; see <a class="closed" href="http://ghc.haskell.org/trac/ghc/ticket/8778#comment:3" title="Comment 3 for Ticket #8778">comment:3</a>.
</p>
<p>
The ticket is still open only because Iavor may add a Note to explain the stuff in subsequent comments.
</p>
<p>
Simon
</p>
TicketcrockeeaTue, 19 Aug 2014 04:47:39 GMT
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:23
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:23
<p>
It doesn't appear to be in 7.8.2. I haven't tried 7.8.3, but I'd rather not upgrade if it's not in there yet.
</p>
TicketsimonpjTue, 19 Aug 2014 06:59:27 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:24
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:24
<ul>
<li><strong>milestone</strong>
changed from <em>⊥</em> to <em>7.10.1</em>
</li>
</ul>
<p>
I don't think it was ever merged onto the 7.8 branch. It's an API change, which we don't usually merge because patch releases aren't supposed to change the API, only fix bugs.
</p>
<p>
So you'll have to wait for 7.10 I'm afraid.
</p>
<p>
Keeping this open, though, pending Iavor's <tt>Note</tt>.
</p>
<p>
Simon
</p>
TicketdiatchkiWed, 20 Aug 2014 23:31:12 GMT
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:25
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:25
<p>
The <tt>Note</tt> about probability of collisions is in <tt>Data.Typeable.Internal</tt> just above the instances. It looks like we are done with this ticket, so I am going to close it.
</p>
TicketdiatchkiWed, 20 Aug 2014 23:32:40 GMTstatus changed
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:26
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:26
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>merge</em>
</li>
</ul>
TicketsimonpjThu, 21 Aug 2014 08:04:14 GMT
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:27
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:27
<p>
For completeness, the note is <tt>Note [Potential Collisions in `Nat` and `Symbol` instances]</tt>.
</p>
<p>
Thanks
</p>
<p>
Simon
</p>
TicketthoughtpoliceMon, 15 Dec 2014 15:15:08 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:28
http://ghc.haskell.org/trac/ghc/ticket/8778#comment:28
<ul>
<li><strong>status</strong>
changed from <em>merge</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
Closing since this is all done.
</p>
Ticket