[GHC] #8697: Type rationals
#8697: Type rationals ------------------------------------+------------------------------------- Reporter: MikeIzbicki | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- 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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8697 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by Fuuzetsu): How do you propose 1/3 is shown with decimal notation? Would this mean there are two different notations around? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8697#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by MikeIzbicki): We could have 1.3 just be sugar for 13/10, so both notations would be acceptable. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8697#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8697#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8697#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by carter): oh, i think that theres support for that in the parser already... have you tried in HEAD? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8697#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8697#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8697#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by dmcclean): * cc: douglas.mcclean@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8697#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8697#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8697#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (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! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8697#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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... 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
#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: | -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8697#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8697: Type rationals -------------------------------------+------------------------------------- Reporter: MikeIzbicki | Owner: (none) 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 dredozubov): 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/Schem... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8697#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC