Opened 4 years ago

# Type rationals

Reported by: Owned by: MikeIzbicki normal Compiler 7.6.3 douglas.mcclean@…, adamgundry Unknown/Multiple Unknown/Multiple None/Unknown

### Description

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

### comment:1 Changed 4 years ago by Fuuzetsu

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

### comment:2 Changed 4 years ago by MikeIzbicki

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

### comment:3 Changed 4 years ago by carter

@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?

### comment:4 Changed 4 years ago by MikeIzbicki

@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)
```

### comment:5 Changed 4 years ago by carter

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

### comment:6 Changed 4 years ago by MikeIzbicki

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?

### comment:7 Changed 4 years ago by carter

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

### comment:9 Changed 4 years ago by MikeIzbicki

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.

### comment:10 Changed 4 years ago by dmcclean

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.

### comment:11 Changed 4 years ago by carter

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!

### comment:12 Changed 22 months ago by adamgundry

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