Type rationals

I've used GHC's Type Nats to implement my own type level rationals (code below). This works fine, but the syntax is a little funky because you have to write out the number as a fraction. For example, you must write 13/10 instead of 1.3; or even worse, 13/1 instead of 13. It would be nice to just write the decimal notation.

I only see one potential problem with this feature: the dot in the decimal notation could interfere with the dot in forall statements. I guess this can be parsed unambiguously, but maybe not.

data Frac = Frac Nat Nat

data instance Sing (n::Frac) = SFrac Integer Integer

instance (SingI a, SingI b) => SingI ('Frac a b) where
    sing = SFrac (fromSing (sing :: Sing a)) (fromSing (sing :: Sing b))

instance Fractional r => SingE (Kind :: Frac) r where
    fromSing (SFrac a b) = fromIntegral a/fromIntegral b

type (/) a b = 'Frac a b

Trac metadata

Trac field	Value
Version	7.6.3
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tfeature request Trac import labels

How do you propose 1/3 is shown with decimal notation? Would this mean there are two different notations around?

We could have 1.3 just be sugar for 13/10, so both notations would be acceptable.

@mike, you could actually use template haskell to write generate type rationals pretty easily. It should also work with 7.6 and earlier ones, though there may be a few corner cases in older ghcs

something like $(makeRatType 7/8) with makeRatType :: Rational -> Q Type being suitably defined.

Have you tried out doing that as a near term solution?

@carter I'm not sure what you're suggesting. The following code (combined with the code above) does exactly what I want:

data Blah (num::Frac) = Blah

f :: Blah num -> Rational
f = ...

g = f (Blah::Blah (13/10))

It would just be nice to be able to write

g = f (Blah::Blah 1.3)

instead.

oh, i think that theres support for that in the parser already... have you tried in HEAD?

I wasn't aware of any GHC support for type level fractions. Any idea what the name of the kind is so I can try it out?

woops, mispoke, i'm a bit exhausted. There is no such support :)

do you have a strawman data model for a type level rationals? Eg using one of the preexisting libraries for type level ints, building up an associated rational set of operations and model types?

Also on the template haskell front, I meant that via template haskell you could do a function that lets you write rationals in decimal notation using template haskell, because decimal numbers can be parsed as rationals.

eg in $(makeRatType 7.3), 7.3 would be turned into rational value. This works at the value level, ableit at template haskell time so you can construct the type

It would also be nice to support negative rationals in a clean way. (For example, by typing just -1.3) I'm guessing this would be best done by adding support for integers, then making the rationals use the integers instead of Nats. This might be confusing for the type checker though because it wouldn't know whether a number like 4 was a type int or a type nat.

Type integers are highly useful in their own right. They are essential to tracking physical dimensions associated with quantities, because you need to track integer powers of length, mass, etc.

so lets decouple this a teeny bit:

a) having good syntactic support for writing numerical literals at the type level: Integers, Nats, Rationals (possibly with floating point style notation)

b) having a satisfactory type model underneath that supports the computations you want to do.

currently in GHC those two are conflated, and perhaps they should be decoupled!

I was prodded by 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:

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

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:

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

Trac metadata

Trac field	Value
CC	douglas.mcclean@gmail.com → adamgundry, douglas.mcclean@gmail.com

I want to say that I would personally like to see type literals for Integers and Rationals. You can always express Rationals as a library, for example, but type levels DSLs can't be really useful without a bit of syntactic sugar to support them.

@adamgundry Considering the direction towards dependent types, I don't think it presents too big of a problem. Type language would have to support a wider array of literals at some anyway. For the state we're in today, singleton types and type literals compliment each other to create an expressive type level DSLs, as can be seen in this library, for an example: https://github.com/dredozubov/schematic/blob/master/src/Data/Schematic/Schema.hs

added Pnormal label

mentioned in issue #18407