Opened 3 years ago
Last modified 13 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@…, adamgundry | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
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 (13)
comment:1 Changed 3 years ago by
comment:2 Changed 3 years ago by
We could have 1.3 just be sugar for 13/10, so both notations would be acceptable.
comment:3 Changed 3 years ago by
@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 3 years ago by
@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 3 years ago by
oh, i think that theres support for that in the parser already... have you tried in HEAD?
comment:6 Changed 3 years ago by
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 3 years ago by
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 3 years ago by
Cc: | douglas.mcclean@… added |
---|
comment:9 Changed 3 years ago by
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 3 years ago by
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 3 years ago by
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 14 months ago by
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 theNum
class at the type level). It would be nice if we could have both42 :: Integer
and42 :: 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...
comment:13 Changed 13 months ago by
Cc: | adamgundry added |
---|
How do you propose 1/3 is shown with decimal notation? Would this mean there are two different notations around?