Opened 18 months ago
Last modified 17 months ago
#8697 new feature request
Type rationals
Reported by: | MikeIzbicki | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 7.6.3 |
Keywords: | Cc: | douglas.mcclean@… | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Revisions: |
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
Change History (11)
comment:1 Changed 18 months ago by Fuuzetsu
comment:2 Changed 17 months ago by MikeIzbicki
We could have 1.3 just be sugar for 13/10, so both notations would be acceptable.
comment:3 Changed 17 months 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 17 months 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)
instead.
comment:5 Changed 17 months ago by carter
oh, i think that theres support for that in the parser already... have you tried in HEAD?
comment:6 Changed 17 months 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 17 months 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:8 Changed 17 months ago by dmcclean
- Cc douglas.mcclean@… added
comment:9 Changed 17 months 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 17 months 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 17 months 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!
How do you propose 1/3 is shown with decimal notation? Would this mean there are two different notations around?