#8697: Type rationals -------------------------------------+------------------------------------- Reporter: MikeIzbicki | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by adamgundry): I was prodded by [https://www.reddit.com/r/haskell/comments/3xoe58/24_days_of_hackage_2015_day... a reddit thread] into thinking about this issue. I agree with Carter that we should treat the syntactic and semantic aspects of this separately. Here's what I said about the syntactic side: Type-level integers/rationals shouldn't be too hard, at least to the level that type-level naturals are currently supported. I think the main thing lacking is a good design for how to write literals (since we don't have `fromInteger` or the `Num` class at the type level). It would be nice if we could have both `42 :: Integer` and `42 :: Nat` in types. One possibility might be to define some (return kind indexed) type families: {{{#!hs type family FromNat (k :: *) (n :: Nat) :: k type instance FromNat Nat n = n type instance FromNat Integer n = ... type instance FromNat Rational n = ... type family FromInteger (k :: *) (i :: Integer) :: k type instance FromInteger Integer i = i type instance FromInteger Rational i = ... type family FromRational (k :: *) (r :: Rational) :: k type instance FromRational Rational r = r }}} Then GHC could translate a numeric literal in a type expression into an application of the appropriate type family (where I'm using suffixes to indicate numeric literals of the underlying kinds): {{{#!hs 42 ~> FromNat k 42n -1 ~> FromInteger k -1i 2.5 ~> FromRational k 2.5r }}} Note that this would allow users to define their own instances of the type families to make use of overloaded numeric literals, for example: {{{#!hs data PNat = Zero | Suc PNat type instance FromNat PNat n = FromPNat n type family FromPNat n where FromPNat 0 = Zero FromPNat n = Suc (FromPNat (n-1)) }}} But perhaps moving the type language further away from the term language isn't such a good idea, considering the general direction of travel towards dependent types... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8697#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler