Opened 4 years ago

Closed 3 years ago

#8778 closed feature request (fixed)

Typeable TypeNats

Reported by: dmcclean Owned by: diatchki
Priority: normal Milestone: 7.10.1
Component: Compiler (Type checker) Version: 7.8.1-rc1
Keywords: Cc: ecrockett0@…, bjorn.buckwalter@…, iavor.diatchki@…, vogt.adam@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: 4385 Differential Rev(s):
Wiki Page:

Description

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.

A Typeable instance for every Nat is the sticking point.

(I do not know if this is even theoretically possible.)

Attachments (1)

Test8778.hs (246 bytes) - added by dmcclean 4 years ago.
Test case

Download all attachments as: .zip

Change History (29)

comment:1 Changed 4 years ago by BjornBuckwalter

Cc: bjorn.buckwalter@… added

comment:2 Changed 4 years ago by carter

@dmcclean could you please explain what you mean? Make up some pseudo code please!

Are you thinking about type level existentials?

comment:3 Changed 4 years ago by thoughtpolice

Version: 7.8.1-rc1

This isn't going to happen in time for 7.8.1.

Changed 4 years ago by dmcclean

Attachment: Test8778.hs added

Test case

comment:4 Changed 4 years ago by dmcclean

Sorry about that, thoughtpolice, I was thinking the field was for where I saw it.

Example (also attached, but here for discussion):

{-# 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)

Results in:

    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.

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).

comment:5 Changed 4 years ago by thoughtpolice

Version: 7.8.1-rc1

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!

comment:6 Changed 4 years ago by dreixel

Cc: iavor.diatchki@… added

Iavor has looked into this, so he might have some status update...

comment:7 Changed 3 years ago by carlhowells

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.

comment:8 Changed 3 years ago by crockeea

Cc: ecrockett0@… added

comment:9 Changed 3 years ago by Iavor S. Diatchki <iavor.diatchki@…>

In 0354fb3676e5b0044601c8e0a5f8039f0cac0c8d/ghc:

Implement `Typeable` support for type-level literals (#8778).

comment:10 Changed 3 years ago by sjoerd_visscher

Should the performance fix from #9203 be applied here too?

comment:11 Changed 3 years ago by diatchki

I'd be happy to make whatever changes are needed, but could you summarize what I should do? The #9203 ticket just talks about HashMaps, and there is a link to Phabricator, but I don't have an account for that...

comment:12 Changed 3 years ago by simonpj

The issue in #9203 is that a Typeable instance should look like

instance Typeable ... where
  typeRep# = \_ -> rep
    where
      rep = ...blah...

and NOT like

instance Typeable ... where
  typeRep# p = ...blah...

to ensure that the computation of rep is shared among all invocations of typeRep#.

So Sjoerd is quite right, I think.

(I'm a bit confused because I thought we only allowed machine-generated instances of Typeable.)

BTW if you have a Github account you automatically have a Phabricator account.

Simon

comment:13 Changed 3 years ago by Iavor S. Diatchki <diatchki@…>

In 836981c7dec5c794ca94408468535cc018dc2e82/ghc:

Redo instance to be more efficient (see #8778, #9203)

comment:14 Changed 3 years ago by diatchki

Aha, thanks for the Phabricator tip!

I redid the instances to be of the form \_ -> blah.

About the Typeable instance: in normal modules we only allow machine-generated instances. The module Data.Typeable.Internal is an exception though---it allows manual instances to accommodate custom instances for some types.

One note about the type-literal instances: they have a much higher chance of collision than a typical kind, as both Nat and Symbol 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.

comment:15 Changed 3 years ago by aavogt

Cc: vogt.adam@… added

comment:16 Changed 3 years ago by simonpj

Re your "note about type-literal instances": did you add a Note with the relevant code. it is 100x times more likely to come to someone's attention there than in this ticket!

Thanks

Simon

comment:17 Changed 3 years ago by diatchki

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.

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:

data Nat = Nil0  | Nil1      | Nil2      | ... | Nil8191
                 | Cons1 Nat | Cons2 Nat | ... | Cons8191 Nat

Pros:

  • Potentially avoids the chance of collisions as now we need to represent only ~16000 constructors, rather than infinitely many.
  • Reasonably sized numbers are represented just as efficiently, and very large numbers are only slightly less efficient.

Cons:

  • A bit slower to compute representation?
  • Functions like splitTyConApp would allow users to observe this encoding, although I am not sure that this matters?

In the "Pros" list I say "potentially" because even though the TypeRep 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...

Thoughts?

comment:18 Changed 3 years ago by diatchki

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.

So, I guess we can close this ticket, unless there are any more issues?

comment:19 Changed 3 years ago by simonpj

I agree. But still worth a Note!

Simon

comment:20 Changed 3 years ago by dmcclean

Thanks, Iavor!

comment:21 Changed 3 years ago by crockeea

What's the milestone for this patch?

comment:22 Changed 3 years ago by simonpj

Owner: set to diatchki

crokeea: I think it's done already; see comment:3.

The ticket is still open only because Iavor may add a Note to explain the stuff in subsequent comments.

Simon

comment:23 Changed 3 years ago by crockeea

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.

comment:24 Changed 3 years ago by simonpj

Milestone: 7.10.1

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.

So you'll have to wait for 7.10 I'm afraid.

Keeping this open, though, pending Iavor's Note.

Simon

comment:25 Changed 3 years ago by diatchki

The Note about probability of collisions is in Data.Typeable.Internal just above the instances. It looks like we are done with this ticket, so I am going to close it.

comment:26 Changed 3 years ago by diatchki

Status: newmerge

comment:27 Changed 3 years ago by simonpj

For completeness, the note is Note [Potential Collisions in `Nat` and `Symbol` instances].

Thanks

Simon

Last edited 3 years ago by simonpj (previous) (diff)

comment:28 Changed 3 years ago by thoughtpolice

Resolution: fixed
Status: mergeclosed

Closing since this is all done.

Note: See TracTickets for help on using tickets.