[GHC] #8697: Type rationals

[GHC]

#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_20_dimensional/cy7mdat?context=3
 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