#8778: Typeable TypeNats --------------------------------------------+------------------------------ Reporter: dmcclean | Owner: Type: feature request | Status: new Priority: normal | Milestone: ⊥ Component: Compiler (Type checker) | Version: 7.8.1-rc1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: 4385 --------------------------------------------+------------------------------ Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8778#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler