[GHC] #12708: RFC: Representation polymorphic Num
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Core | Version: 8.0.1 Libraries | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I can create a GHC proposal for this but I need a sanity check first {{{#!hs import Prelude hiding (Num (..)) import qualified Prelude as P import GHC.Prim import GHC.Types class Num (a :: Type k) where (+) :: a -> a -> a (-) :: a -> a -> a (*) :: a -> a -> a negate :: a -> a abs :: a -> a signum :: a -> a fromInteger :: Integer -> a instance Num Int# where (+) :: Int# -> Int# -> Int# (+) = (+#) (-) :: Int# -> Int# -> Int# (-) = (-#) (*) :: Int# -> Int# -> Int# (*) = (*#) negate :: Int# -> Int# negate = negateInt# ... fromInteger :: Integer -> Int# fromInteger (fromInteger -> I# int) = int instance Num Double# where (+) :: Double# -> Double# -> Double# (+) = (+##) (-) :: Double# -> Double# -> Double# (-) = (-##) (*) :: Double# -> Double# -> Double# (*) = (*##) negate :: Double# -> Double# negate = negateDouble# ... fromInteger :: Integer -> Double# fromInteger (fromInteger -> D# dbl) = dbl }}} Note how the `fromInteger` views aren't qualified? That's because we can branch on the kind and all of a sudden, all instances of old `Num` are instances of our `Num` {{{#!hs instance P.Num a => Num (a :: Type) where (+) = (P.+) (-) = (P.-) (*) = (P.*) negate = P.negate abs = P.abs signum = P.signum fromInteger = P.fromInteger }}} ---- Same with `Show` etc. etc. {{{#!hs class Show (a :: TYPE k) where show :: (a :: TYPE k) -> String instance P.Show a => Show (a :: Type) where show :: (a :: Type) -> String show = P.show instance Show Int# where show :: Int# -> String show int = show (I# int) instance Show Double# where show :: Double# -> String show dbl = show (D# dbl) }}} ---- What effects would this have? They are even printed the same by default {{{#!hs
:kind Prelude.Num Prelude.Num :: * -> Constraint :kind Main.Num Main.Num :: * -> Constraint :set -fprint-explicit-runtime-reps :kind Main.Num Main.Num :: TYPE k -> Constraint }}}
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 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 Iceland_jack): (I am concerned that it seems the instance resolution defaults to `Type`.. if I remove the instances (and qualify the `fromInteger` views) {{{#!hs -- × × × REMOVED × × × -- instance P.Num a => Num (a :: Type) where -- instance P.Show a => Show (a :: Type) where }}} the types of `show` and `(+)` are (let's give it a module name `UU`) {{{#!hs UU.fromInteger :: UU.Num a => Integer -> a (UU.+) :: UU.Num a => a -> a -> a UU.show :: UU.Show a => a -> String }}} whereas with those instances it seems to default to the `Type`, is this intended! {{{#!hs UU.fromInteger :: Prelude.Num a => Integer -> a (UU.+) :: Prelude.Num a => a -> a -> a (UU.show') :: Prelude.Show a => a -> String }}} ) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 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 Iceland_jack): With it and `RebindableSyntax` you can write {{{#!hs foo :: Int foo = I# u + 10 * 4 where u :: Int# u = 10 + 10 * 4 bar :: String bar = show @PtrRepLifted @Int 24 ++ show @IntRep @Int# 24 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 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 Iceland_jack): Should this not be allowed when `minBound :: () -> a` is allowed? {{{#!hs class Bounded (TYPE rep) where minBound :: a minBound :: a }}} for {{{#!hs instance Bounded Int# where minBound :: Int# minBound = -9223372036854775808# maxBound :: Int# maxBound = 9223372036854775807# }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 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 Iceland_jack): {{{#!hs instance Eq (MutVar# s a) where (==) :: MutVar# s a -> MutVar# s a -> Bool a == b = isTrue# (sameMutVar# a b) instance Eq (MVar# s a) where (==) :: MVar# s a -> MVar# s a -> Bool a == b = isTrue# (sameMVar# a b) instance Eq (TVar# s a) where (==) :: TVar# s a -> TVar# s a -> Bool a == b = isTrue# (sameTVar# a b) instance Eq (StableName# a) where (==) :: StableName# a -> StableName# a -> Bool a == b = isTrue# (eqStableName# a b) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 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: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: @@ -93,0 +93,9 @@ + {{{#!hs + class Functor (f :: Type -> TYPE rep) where + fmap :: (a -> b) -> (f a -> f b) + + instance Functor ((# , #) a) where + fmap :: (b -> b') -> ((# a, b #) -> (# a, b'#)) + fmap f (# a, b #) = (# a, f b #) + }}} + @@ -98,1 +107,0 @@ - >>> :kind Prelude.Num @@ -100,0 +108,7 @@ + Main.Num :: * -> Constraint + + -- >>> :set -fprint-explicit-runtime-reps + Prelude.Num :: * -> Constraint + Main.Num :: TYPE k -> Constraint + + >>> :set -Wprint-explicit-runtime-rep @@ -101,4 +116,3 @@ - Main.Num :: * -> Constraint - >>> :set -fprint-explicit-runtime-reps - >>> :kind Main.Num - Main.Num :: TYPE k -> Constraint + Main.Num :: forall (k :: RuntimeRep). TYPE k -> Constraint + + New description: I can create a GHC proposal for this but I need a sanity check first {{{#!hs import Prelude hiding (Num (..)) import qualified Prelude as P import GHC.Prim import GHC.Types class Num (a :: Type k) where (+) :: a -> a -> a (-) :: a -> a -> a (*) :: a -> a -> a negate :: a -> a abs :: a -> a signum :: a -> a fromInteger :: Integer -> a instance Num Int# where (+) :: Int# -> Int# -> Int# (+) = (+#) (-) :: Int# -> Int# -> Int# (-) = (-#) (*) :: Int# -> Int# -> Int# (*) = (*#) negate :: Int# -> Int# negate = negateInt# ... fromInteger :: Integer -> Int# fromInteger (fromInteger -> I# int) = int instance Num Double# where (+) :: Double# -> Double# -> Double# (+) = (+##) (-) :: Double# -> Double# -> Double# (-) = (-##) (*) :: Double# -> Double# -> Double# (*) = (*##) negate :: Double# -> Double# negate = negateDouble# ... fromInteger :: Integer -> Double# fromInteger (fromInteger -> D# dbl) = dbl }}} Note how the `fromInteger` views aren't qualified? That's because we can branch on the kind and all of a sudden, all instances of old `Num` are instances of our `Num` {{{#!hs instance P.Num a => Num (a :: Type) where (+) = (P.+) (-) = (P.-) (*) = (P.*) negate = P.negate abs = P.abs signum = P.signum fromInteger = P.fromInteger }}} ---- Same with `Show` etc. etc. {{{#!hs class Show (a :: TYPE k) where show :: (a :: TYPE k) -> String instance P.Show a => Show (a :: Type) where show :: (a :: Type) -> String show = P.show instance Show Int# where show :: Int# -> String show int = show (I# int) instance Show Double# where show :: Double# -> String show dbl = show (D# dbl) }}} {{{#!hs class Functor (f :: Type -> TYPE rep) where fmap :: (a -> b) -> (f a -> f b) instance Functor ((# , #) a) where fmap :: (b -> b') -> ((# a, b #) -> (# a, b'#)) fmap f (# a, b #) = (# a, f b #) }}} ---- What effects would this have? They are even printed the same by default {{{#!hs Prelude.Num :: * -> Constraint Main.Num :: * -> Constraint -- >>> :set -fprint-explicit-runtime-reps Prelude.Num :: * -> Constraint Main.Num :: TYPE k -> Constraint
:set -Wprint-explicit-runtime-rep :kind Main.Num Main.Num :: forall (k :: RuntimeRep). TYPE k -> Constraint
}}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 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: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: @@ -114,5 +114,3 @@ - >>> :set -Wprint-explicit-runtime-rep - >>> :kind Main.Num - Main.Num :: forall (k :: RuntimeRep). TYPE k -> Constraint - - + -- >>> :set -Wprint-explicit-runtime-rep + Prelude.Num :: * -> Constraint + Main.Num :: forall (k :: RuntimeRep). TYPE k -> Constraint New description: I can create a GHC proposal for this but I need a sanity check first {{{#!hs import Prelude hiding (Num (..)) import qualified Prelude as P import GHC.Prim import GHC.Types class Num (a :: Type k) where (+) :: a -> a -> a (-) :: a -> a -> a (*) :: a -> a -> a negate :: a -> a abs :: a -> a signum :: a -> a fromInteger :: Integer -> a instance Num Int# where (+) :: Int# -> Int# -> Int# (+) = (+#) (-) :: Int# -> Int# -> Int# (-) = (-#) (*) :: Int# -> Int# -> Int# (*) = (*#) negate :: Int# -> Int# negate = negateInt# ... fromInteger :: Integer -> Int# fromInteger (fromInteger -> I# int) = int instance Num Double# where (+) :: Double# -> Double# -> Double# (+) = (+##) (-) :: Double# -> Double# -> Double# (-) = (-##) (*) :: Double# -> Double# -> Double# (*) = (*##) negate :: Double# -> Double# negate = negateDouble# ... fromInteger :: Integer -> Double# fromInteger (fromInteger -> D# dbl) = dbl }}} Note how the `fromInteger` views aren't qualified? That's because we can branch on the kind and all of a sudden, all instances of old `Num` are instances of our `Num` {{{#!hs instance P.Num a => Num (a :: Type) where (+) = (P.+) (-) = (P.-) (*) = (P.*) negate = P.negate abs = P.abs signum = P.signum fromInteger = P.fromInteger }}} ---- Same with `Show` etc. etc. {{{#!hs class Show (a :: TYPE k) where show :: (a :: TYPE k) -> String instance P.Show a => Show (a :: Type) where show :: (a :: Type) -> String show = P.show instance Show Int# where show :: Int# -> String show int = show (I# int) instance Show Double# where show :: Double# -> String show dbl = show (D# dbl) }}} {{{#!hs class Functor (f :: Type -> TYPE rep) where fmap :: (a -> b) -> (f a -> f b) instance Functor ((# , #) a) where fmap :: (b -> b') -> ((# a, b #) -> (# a, b'#)) fmap f (# a, b #) = (# a, f b #) }}} ---- What effects would this have? They are even printed the same by default {{{#!hs Prelude.Num :: * -> Constraint Main.Num :: * -> Constraint -- >>> :set -fprint-explicit-runtime-reps Prelude.Num :: * -> Constraint Main.Num :: TYPE k -> Constraint -- >>> :set -Wprint-explicit-runtime-rep Prelude.Num :: * -> Constraint Main.Num :: forall (k :: RuntimeRep). TYPE k -> Constraint }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 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: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: @@ -114,1 +114,1 @@ - -- >>> :set -Wprint-explicit-runtime-rep + -- >>> :set -fprint-explicit-foralls New description: I can create a GHC proposal for this but I need a sanity check first {{{#!hs import Prelude hiding (Num (..)) import qualified Prelude as P import GHC.Prim import GHC.Types class Num (a :: Type k) where (+) :: a -> a -> a (-) :: a -> a -> a (*) :: a -> a -> a negate :: a -> a abs :: a -> a signum :: a -> a fromInteger :: Integer -> a instance Num Int# where (+) :: Int# -> Int# -> Int# (+) = (+#) (-) :: Int# -> Int# -> Int# (-) = (-#) (*) :: Int# -> Int# -> Int# (*) = (*#) negate :: Int# -> Int# negate = negateInt# ... fromInteger :: Integer -> Int# fromInteger (fromInteger -> I# int) = int instance Num Double# where (+) :: Double# -> Double# -> Double# (+) = (+##) (-) :: Double# -> Double# -> Double# (-) = (-##) (*) :: Double# -> Double# -> Double# (*) = (*##) negate :: Double# -> Double# negate = negateDouble# ... fromInteger :: Integer -> Double# fromInteger (fromInteger -> D# dbl) = dbl }}} Note how the `fromInteger` views aren't qualified? That's because we can branch on the kind and all of a sudden, all instances of old `Num` are instances of our `Num` {{{#!hs instance P.Num a => Num (a :: Type) where (+) = (P.+) (-) = (P.-) (*) = (P.*) negate = P.negate abs = P.abs signum = P.signum fromInteger = P.fromInteger }}} ---- Same with `Show` etc. etc. {{{#!hs class Show (a :: TYPE k) where show :: (a :: TYPE k) -> String instance P.Show a => Show (a :: Type) where show :: (a :: Type) -> String show = P.show instance Show Int# where show :: Int# -> String show int = show (I# int) instance Show Double# where show :: Double# -> String show dbl = show (D# dbl) }}} {{{#!hs class Functor (f :: Type -> TYPE rep) where fmap :: (a -> b) -> (f a -> f b) instance Functor ((# , #) a) where fmap :: (b -> b') -> ((# a, b #) -> (# a, b'#)) fmap f (# a, b #) = (# a, f b #) }}} ---- What effects would this have? They are even printed the same by default {{{#!hs Prelude.Num :: * -> Constraint Main.Num :: * -> Constraint -- >>> :set -fprint-explicit-runtime-reps Prelude.Num :: * -> Constraint Main.Num :: TYPE k -> Constraint -- >>> :set -fprint-explicit-foralls Prelude.Num :: * -> Constraint Main.Num :: forall (k :: RuntimeRep). TYPE k -> Constraint }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 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: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: @@ -100,0 +100,18 @@ + + class Applicative (f :: Type -> TYPE rep) where + pure :: a -> f a + (<*>) :: f (a -> b) -> (f a -> f b) + + instance Monoid m => Applicative ((# , #) m) where + pure :: a -> (# m, a #) + pure a = (# mempty, a #) + + (<*>) :: (# m, a -> b #) -> ((# m, a #) -> (# m, b #)) + (# m1, f #) <*> (# m2, x #) = (# m1 <> m2, f x #) + + class Foldable (f :: Type -> TYPE rep) where + fold :: Monoid m => f m -> m + + instance Foldable ((# , #) xx) where + fold :: Monoid m => (# xx, m #) -> m + fold (# _, m #) = m @@ -101,0 +119,2 @@ + + halp where does this end New description: I can create a GHC proposal for this but I need a sanity check first {{{#!hs import Prelude hiding (Num (..)) import qualified Prelude as P import GHC.Prim import GHC.Types class Num (a :: Type k) where (+) :: a -> a -> a (-) :: a -> a -> a (*) :: a -> a -> a negate :: a -> a abs :: a -> a signum :: a -> a fromInteger :: Integer -> a instance Num Int# where (+) :: Int# -> Int# -> Int# (+) = (+#) (-) :: Int# -> Int# -> Int# (-) = (-#) (*) :: Int# -> Int# -> Int# (*) = (*#) negate :: Int# -> Int# negate = negateInt# ... fromInteger :: Integer -> Int# fromInteger (fromInteger -> I# int) = int instance Num Double# where (+) :: Double# -> Double# -> Double# (+) = (+##) (-) :: Double# -> Double# -> Double# (-) = (-##) (*) :: Double# -> Double# -> Double# (*) = (*##) negate :: Double# -> Double# negate = negateDouble# ... fromInteger :: Integer -> Double# fromInteger (fromInteger -> D# dbl) = dbl }}} Note how the `fromInteger` views aren't qualified? That's because we can branch on the kind and all of a sudden, all instances of old `Num` are instances of our `Num` {{{#!hs instance P.Num a => Num (a :: Type) where (+) = (P.+) (-) = (P.-) (*) = (P.*) negate = P.negate abs = P.abs signum = P.signum fromInteger = P.fromInteger }}} ---- Same with `Show` etc. etc. {{{#!hs class Show (a :: TYPE k) where show :: (a :: TYPE k) -> String instance P.Show a => Show (a :: Type) where show :: (a :: Type) -> String show = P.show instance Show Int# where show :: Int# -> String show int = show (I# int) instance Show Double# where show :: Double# -> String show dbl = show (D# dbl) }}} {{{#!hs class Functor (f :: Type -> TYPE rep) where fmap :: (a -> b) -> (f a -> f b) instance Functor ((# , #) a) where fmap :: (b -> b') -> ((# a, b #) -> (# a, b'#)) fmap f (# a, b #) = (# a, f b #) class Applicative (f :: Type -> TYPE rep) where pure :: a -> f a (<*>) :: f (a -> b) -> (f a -> f b) instance Monoid m => Applicative ((# , #) m) where pure :: a -> (# m, a #) pure a = (# mempty, a #) (<*>) :: (# m, a -> b #) -> ((# m, a #) -> (# m, b #)) (# m1, f #) <*> (# m2, x #) = (# m1 <> m2, f x #) class Foldable (f :: Type -> TYPE rep) where fold :: Monoid m => f m -> m instance Foldable ((# , #) xx) where fold :: Monoid m => (# xx, m #) -> m fold (# _, m #) = m }}} halp where does this end ---- What effects would this have? They are even printed the same by default {{{#!hs Prelude.Num :: * -> Constraint Main.Num :: * -> Constraint -- >>> :set -fprint-explicit-runtime-reps Prelude.Num :: * -> Constraint Main.Num :: TYPE k -> Constraint -- >>> :set -fprint-explicit-foralls Prelude.Num :: * -> Constraint Main.Num :: forall (k :: RuntimeRep). TYPE k -> Constraint }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 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 Iceland_jack): With the upcoming `UnboxedSums` {{{#!hs instance (Eq a, Eq b) => Eq (# a | b #) where (==) :: (# a | b #) -> (# a | b #) -> Bool (# a | #) == (# a' | #) = a == a' (# | b #) == (# | b' #) = b == b' _ == _ = False }}} In GHCi, version 8.1.20160930 it seems like you cannot partially apply unboxed sums `(# | #)` so I can't write {{{#!hs instance Functor ((# | #) a) instance Applicative ((# | #) a) instance Foldable ((# | #) a) ... }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 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 goldfire): By gum, this is bloody brilliant. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 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 goldfire): Replying to [comment:3 Iceland_jack]:
Should this not be allowed when `minBound :: () -> a` is allowed?
Because `blah :: Int#` is not allowed? This would actually be OK, because methods -- even nullary ones, like `minBound` are actually functions that take dictionaries. So we're OK here. And to your question in comment:2: You won't be able to supply a default implementation of these functions because of the Golden Rule of Representation Polymorphism: You may never bind a variable whose type is representation polymorphic. Your default implementation violates this rule. I'm wondering if a `default` type signature can help, somehow, but I don't see how to write it: there's no way of saying `NotAVariable k` as a constraint. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 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 nomeata):
By gum, this is brilliant.
He wanted a sanity check, not a brilliance check :-) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 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 Iceland_jack): If we did like [https://github.com/mikeizbicki/subhask subhask] we could even interpret `==` in a different logic {{{#!hs -- This doesn't work unless it's closed type family Rep (rep :: RuntimeRep) :: RuntimeRep where Rep IntRep = IntRep Rep DoubleRep = IntRep Rep PtrRepUnlifted = IntRep Rep PtrRepLifted = PtrRepLifted -- etc. class Eq (a :: TYPE rep) where type Logic (a :: TYPE rep) :: TYPE (Rep rep) (==) :: a -> a -> Logic a instance Eq (Int :: Type) where type Logic Int = Bool (==) :: Int -> Int -> Bool (f == g) a = f a == g a instance Eq (Int# :: TYPE IntRep) where type Logic Int# = Int# (==) :: Int# -> Int# -> Int# (==) = (==#) instance Eq (Double# :: TYPE DoubleRep) where type Logic Double# = Int# (==) :: Double# -> Double# -> Int# (==) = (==##) }}} Come on, you know you want it ;) we can use the same `==` for EDSLs? {{{#!hs data Exp :: Type -> Type where Eq :: a -> a -> Exp Bool instance Eq (Exp a) where type Logic (Exp a) = Exp Bool (==) :: Exp a -> Exp a -> Exp Bool (==) = Eq }}} or {{{#!hs data TY = INT | BOOL data Exp :: TY -> Type where EqI :: INT -> INT -> Exp BOOL EqB :: BOOL -> BOOL -> Exp BOOL instance Eq (Exp INT) where type Logic (Exp INT) = Exp BOOL (==) :: Exp INT -> Exp INT -> Exp BOOL (==) = EqI instance Eq (Exp BOOL) where type Logic (Exp BOOL) = Exp BOOL (==) :: Exp BOOL -> Exp BOOL -> Exp BOOL (==) = EqB }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 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 goldfire): I think your first '''Edit:''' in comment:13 is orthogonal to the overall ticket and could be accomplished by generalizing `Eq` along similar lines to what you've done but without representation polymorphism. And we must be careful: while this is a new sword that slays many beasts, it doesn't slay ''all'' beasts, nor should we expect it to. Your '''Edit 2''' looks like a beast it doesn't slay. Some smart design will be needed for us to learn how to wield this sword, and I would favor implementing this all in a library for a cycle before thinking about moving anything into `base`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 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 Iceland_jack): I personally find this beautiful (and it made me think of a solution to something I promised to email you a long time ago Richard, correspondence is not my strong suit) {{{#!hs instance P.Num a => Num (a :: Type) where (+) :: a -> a -> a (+) = (+#) -- ... instance P.Show a => Show (a :: Type) where show :: (a :: Type) -> String show = P.show }}} so I believe this could easily be an “alternate” Prelude, people continue to define instances for `Prelude.Num` which makes them instances of our runtime-representation polymorphic `Num`. A great benefit of `Num` is that I can write {{{#!hs ten :: Num a => a ten = 1 + 2 + 3 + 4 }}} and later define my own type, and it was as if `ten` had been defined with it in mind: {{{#!hs data Exp = I Integer | Exp :+: Exp | ... instance Num Exp where (+) :: Exp -> Exp -> Exp (+) = (:+:) fromInteger :: Integer -> Exp fromInteger = I -- >>> ten :: Exp -- ((I 1 :+: I 2) :+: I 3) :+: I 4 }}} Trouble is `ten` must be lifted (`ten :: Prelude.Num a => a`) so we cannot pass it to `I#`, but we can write {{{#!hs reNum :: (forall a. P.Num a => a) -> (forall rep (b :: TYPE rep). Num b => b) reNum f = fromInteger (f @Integer) ten' :: forall rep (a :: TYPE rep). Num a => a ten' = reNum ten }}} which constant folds the rich structure `((I 1 :+: I 2) :+: I 3) :+: I 4` into `I 10 :: Exp` but it's fine for `I# (ten' :: Int#)` (which does work in HEAD). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 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 Iceland_jack): This is a pipe dream, `Logic` offers cool possibilities. [https://hackage.haskell.org/package/sbv-5.12/docs/src/Data-SBV- BitVectors-Model.html sbv] has `EqSymbolic` which is an `Eq a` where `Logic a ~ SBool` : {{{#!hs infix 4 .==, ./= class EqSymbolic a where (.==), (./=) :: a -> a -> SBool }}} This could be the regular `Eq` if we had something like (with `Boolean` taken from ticket:10592#comment:12) {{{#!hs class Boolean (Logic a) => Eq (a :: TYPE rep) where type Logic a :: TYPE (Rep rep) (==) :: a -> a -> Logic a a == b = not (a /= b) (/=) :: a -> a -> Logic a a /= b = not (a == b) instance Eq (SBV a) where type Logic (SBV a) = SBool (==) :: SBV a -> SBV a -> SBool SBV a == SBV b = SBV (svEqual a b) instance EqSymbolic (SArray a b) where type Logic (SArray a b) = SBool (==) :: SArray a b -> SArray a b -> SBool SArray a == SArray b = SBV (eqSArr a b) }}} We lose `EqSymbolic Bool` but `... => EqSymbolic [a]` would survive in a different form. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 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 bgamari): Simon and Richard's recent PLDI paper on [[https://www.microsoft.com/en- us/research/publication/levity-polymorphism/|levity polymorphism]] is quite relevant to this ticket (and in fact cites it). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 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: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: @@ -9,1 +9,1 @@ - class Num (a :: Type k) where + class Num (a :: TYPE k) where @@ -35,1 +35,1 @@ - fromInteger (fromInteger -> I# int) = int + fromInteger (fromInteger @PtrRepLifted @Int -> I# int) = int @@ -54,1 +54,1 @@ - fromInteger (fromInteger -> D# dbl) = dbl + fromInteger (fromInteger @PtrRepLifted @Double -> D# dbl) = dbl @@ -63,7 +63,7 @@ - (+) = (P.+) - (-) = (P.-) - (*) = (P.*) - negate = P.negate - abs = P.abs - signum = P.signum - fromInteger = P.fromInteger + (+) = (P.+) @a + (-) = (P.-) @a + (*) = (P.*) @a + negate = P.negate @a + abs = P.abs @a + signum = P.signum @a + fromInteger = P.fromInteger @a @@ -82,1 +82,1 @@ - show = P.show + show = P.show @a @@ -84,1 +84,1 @@ - instance Show Int# where + instance Show (Int# :: TYPE IntRep) where @@ -86,1 +86,1 @@ - show int = show (I# int) + show int = show @PtrRepLifted @Int (I# int) @@ -88,1 +88,1 @@ - instance Show Double# where + instance Show (Double# :: TYPE DoubleRep) where @@ -90,1 +90,1 @@ - show dbl = show (D# dbl) + show dbl = show @PtrRepLifted @Double (D# dbl) New description: I can create a GHC proposal for this but I need a sanity check first {{{#!hs import Prelude hiding (Num (..)) import qualified Prelude as P import GHC.Prim import GHC.Types class Num (a :: TYPE k) where (+) :: a -> a -> a (-) :: a -> a -> a (*) :: a -> a -> a negate :: a -> a abs :: a -> a signum :: a -> a fromInteger :: Integer -> a instance Num Int# where (+) :: Int# -> Int# -> Int# (+) = (+#) (-) :: Int# -> Int# -> Int# (-) = (-#) (*) :: Int# -> Int# -> Int# (*) = (*#) negate :: Int# -> Int# negate = negateInt# ... fromInteger :: Integer -> Int# fromInteger (fromInteger @PtrRepLifted @Int -> I# int) = int instance Num Double# where (+) :: Double# -> Double# -> Double# (+) = (+##) (-) :: Double# -> Double# -> Double# (-) = (-##) (*) :: Double# -> Double# -> Double# (*) = (*##) negate :: Double# -> Double# negate = negateDouble# ... fromInteger :: Integer -> Double# fromInteger (fromInteger @PtrRepLifted @Double -> D# dbl) = dbl }}} Note how the `fromInteger` views aren't qualified? That's because we can branch on the kind and all of a sudden, all instances of old `Num` are instances of our `Num` {{{#!hs instance P.Num a => Num (a :: Type) where (+) = (P.+) @a (-) = (P.-) @a (*) = (P.*) @a negate = P.negate @a abs = P.abs @a signum = P.signum @a fromInteger = P.fromInteger @a }}} ---- Same with `Show` etc. etc. {{{#!hs class Show (a :: TYPE k) where show :: (a :: TYPE k) -> String instance P.Show a => Show (a :: Type) where show :: (a :: Type) -> String show = P.show @a instance Show (Int# :: TYPE IntRep) where show :: Int# -> String show int = show @PtrRepLifted @Int (I# int) instance Show (Double# :: TYPE DoubleRep) where show :: Double# -> String show dbl = show @PtrRepLifted @Double (D# dbl) }}} {{{#!hs class Functor (f :: Type -> TYPE rep) where fmap :: (a -> b) -> (f a -> f b) instance Functor ((# , #) a) where fmap :: (b -> b') -> ((# a, b #) -> (# a, b'#)) fmap f (# a, b #) = (# a, f b #) class Applicative (f :: Type -> TYPE rep) where pure :: a -> f a (<*>) :: f (a -> b) -> (f a -> f b) instance Monoid m => Applicative ((# , #) m) where pure :: a -> (# m, a #) pure a = (# mempty, a #) (<*>) :: (# m, a -> b #) -> ((# m, a #) -> (# m, b #)) (# m1, f #) <*> (# m2, x #) = (# m1 <> m2, f x #) class Foldable (f :: Type -> TYPE rep) where fold :: Monoid m => f m -> m instance Foldable ((# , #) xx) where fold :: Monoid m => (# xx, m #) -> m fold (# _, m #) = m }}} halp where does this end ---- What effects would this have? They are even printed the same by default {{{#!hs Prelude.Num :: * -> Constraint Main.Num :: * -> Constraint -- >>> :set -fprint-explicit-runtime-reps Prelude.Num :: * -> Constraint Main.Num :: TYPE k -> Constraint -- >>> :set -fprint-explicit-foralls Prelude.Num :: * -> Constraint Main.Num :: forall (k :: RuntimeRep). TYPE k -> Constraint }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 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 Iceland_jack): Using the generalized function composition from the paper {{{#!hs (·) :: forall (r :: RuntimeRep) (a :: Type) (b :: Type) (c :: TYPE r). (b -> c) -> (a -> b) -> (a -> c) (f · g) x = f (g x) }}} we can write {{{#!hs fromInteger :: Integer -> Int# fromInteger (fromInteger -> I# i) = i fromInteger :: Integer -> Int# fromInteger (fromInteger -> D# d) = d) }}} pointfree {{{#!hs fromInteger :: Integer -> Int# fromInteger = getInt# · fromInteger where getInt# :: Int -> Int# getInt# (I# i) = i fromInteger :: Integer -> Double# fromInteger = getDouble# · fromInteger where getDouble# :: Double -> Double# getDouble# (D# d) = d -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism 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 simonpj): * keywords: => LevityPolymorphism -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism 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 changed by Iceland_jack: @@ -98,1 +98,1 @@ - fmap :: (b -> b') -> ((# a, b #) -> (# a, b'#)) + fmap :: (b -> b') -> ((# a, b #) -> (# a, b' #)) @@ -105,1 +105,1 @@ - instance Monoid m => Applicative ((# , #) m) where + instance Monoid m => Applicative ((# , #) m) where New description: I can create a GHC proposal for this but I need a sanity check first {{{#!hs import Prelude hiding (Num (..)) import qualified Prelude as P import GHC.Prim import GHC.Types class Num (a :: TYPE k) where (+) :: a -> a -> a (-) :: a -> a -> a (*) :: a -> a -> a negate :: a -> a abs :: a -> a signum :: a -> a fromInteger :: Integer -> a instance Num Int# where (+) :: Int# -> Int# -> Int# (+) = (+#) (-) :: Int# -> Int# -> Int# (-) = (-#) (*) :: Int# -> Int# -> Int# (*) = (*#) negate :: Int# -> Int# negate = negateInt# ... fromInteger :: Integer -> Int# fromInteger (fromInteger @PtrRepLifted @Int -> I# int) = int instance Num Double# where (+) :: Double# -> Double# -> Double# (+) = (+##) (-) :: Double# -> Double# -> Double# (-) = (-##) (*) :: Double# -> Double# -> Double# (*) = (*##) negate :: Double# -> Double# negate = negateDouble# ... fromInteger :: Integer -> Double# fromInteger (fromInteger @PtrRepLifted @Double -> D# dbl) = dbl }}} Note how the `fromInteger` views aren't qualified? That's because we can branch on the kind and all of a sudden, all instances of old `Num` are instances of our `Num` {{{#!hs instance P.Num a => Num (a :: Type) where (+) = (P.+) @a (-) = (P.-) @a (*) = (P.*) @a negate = P.negate @a abs = P.abs @a signum = P.signum @a fromInteger = P.fromInteger @a }}} ---- Same with `Show` etc. etc. {{{#!hs class Show (a :: TYPE k) where show :: (a :: TYPE k) -> String instance P.Show a => Show (a :: Type) where show :: (a :: Type) -> String show = P.show @a instance Show (Int# :: TYPE IntRep) where show :: Int# -> String show int = show @PtrRepLifted @Int (I# int) instance Show (Double# :: TYPE DoubleRep) where show :: Double# -> String show dbl = show @PtrRepLifted @Double (D# dbl) }}} {{{#!hs class Functor (f :: Type -> TYPE rep) where fmap :: (a -> b) -> (f a -> f b) instance Functor ((# , #) a) where fmap :: (b -> b') -> ((# a, b #) -> (# a, b' #)) fmap f (# a, b #) = (# a, f b #) class Applicative (f :: Type -> TYPE rep) where pure :: a -> f a (<*>) :: f (a -> b) -> (f a -> f b) instance Monoid m => Applicative ((# , #) m) where pure :: a -> (# m, a #) pure a = (# mempty, a #) (<*>) :: (# m, a -> b #) -> ((# m, a #) -> (# m, b #)) (# m1, f #) <*> (# m2, x #) = (# m1 <> m2, f x #) class Foldable (f :: Type -> TYPE rep) where fold :: Monoid m => f m -> m instance Foldable ((# , #) xx) where fold :: Monoid m => (# xx, m #) -> m fold (# _, m #) = m }}} halp where does this end ---- What effects would this have? They are even printed the same by default {{{#!hs Prelude.Num :: * -> Constraint Main.Num :: * -> Constraint -- >>> :set -fprint-explicit-runtime-reps Prelude.Num :: * -> Constraint Main.Num :: TYPE k -> Constraint -- >>> :set -fprint-explicit-foralls Prelude.Num :: * -> Constraint Main.Num :: forall (k :: RuntimeRep). TYPE k -> Constraint }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism 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 goldfire): I still believe this is a great idea and would welcome a formal proposal about this. I also still believe that this is something better done in a library for a release or so before we start mucking with something so fundamental. There's nothing about this that cannot be done in a library (modulo `RebindableSyntax`). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism 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 Iceland_jack): Replying to [comment:22 goldfire]:
I still believe this is a great idea and would welcome a formal proposal about this.
[https://github.com/ghc-proposals/ghc-proposals/pull/30 Done]. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
I still believe this is a great idea and would welcome a formal proposal about this. I also still believe that this is something better done in a
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism 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 carter): Replying to [comment:22 goldfire]: library for a release or so before we start mucking with something so fundamental. There's nothing about this that cannot be done in a library (modulo `RebindableSyntax`). I agree with richard, experimental changes to the core num prelude, especially those using still new constructs should happen in userland first. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism 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 oerjan): * cc: oerjan (added) Comment: Replying to [comment:11 goldfire]:
Replying to [comment:3 Iceland_jack]:
Should this not be allowed when `minBound :: () -> a` is allowed?
Because `blah :: Int#` is not allowed? This would actually be OK, because methods -- even nullary ones, like `minBound` are actually functions that take dictionaries. So we're OK here.
The question is, how would you store the necessary `Int#` in the dictionary? It seems to me you'd have to use some kind of indirection because otherwise you have a dictionary field than can have arbitrary size. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism 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 goldfire): Replying to [comment:25 oerjan]:
The question is, how would you store the necessary `Int#` in the dictionary? It seems to me you'd have to use some kind of indirection because otherwise you have a dictionary field than can have arbitrary size.
Spot on. You're right -- we would have a problem with `Bounded`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:26 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: 12980 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * related: => 12980 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:27 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12980 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by oerjan): * related: 12980 => #12980 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:28 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12980 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): An exhaustive search through `ghc-prim` and `base` found 34 (!) classes that can be generalized this way: {{{ Eq, Ord, Functor, Applicative, Monad, MonadFail, MonadFix, MonadIO, Bifoldable, Bifunctor, HasResolution, Foldable, Eq1, Ord1, Eq2, Ord2, IsString, TestCoercion, TestEquality, Storable, IsList, Num, Real, Fractional, Generic, Generic1, GHCiSandboxIO, BufferedIO, RawIO, IsLabel, PrintfType, HPrintfType, PrintfArg, IsChar }}} Some are surely more useful to generalize than others. But wow! More classes morally could be included in this list but for two limiting factors: - Many classes use lists somewhere. (For example, `Show`.) However, we could define a family of list types, one for each representation (which would box unboxed tuples), and then use a type family to select the appropriate list type, allowing generalizations of classes that use lists. - Several classes (e.g., `Integral`) use tuples, preventing generalization. But we could just use unboxed tuples and away we go. Another annoyance was that `Applicative` can be generalized to make its parameter `f :: Type -> TYPE r`, but not `f :: TYPE r1 -> TYPE r2`. The latter is impossible because the class definition mentions `f (a -> b)`, and functions are always lifted. It would be lovely, though, to ponder the possibility of `class Applicative (f :: forall (r1 :: RuntimeRep). TYPE r1 -> TYPE r2)`, where `Applicative` would then have a higher-rank kind. And, we could generalize `IO` (it's implemented using an unboxed tuple, after all) and then `IO` could be made an instance of this new `Applicative`. `Monad` would soon follow, and you'd then be able to return unboxed values in `do`-notation. A final note: In testing all this, I had to add `default` signatures imposing a `r ~ LiftedRep` constraint whenever a generalized class had a default implementation, because the default implementation would work only at kind `Type`. This works, but it's disappointing that there can be no defaults at representations other than `LiftedRep`. However, I've realized we ''can''. Instead of `r ~ LiftedRep` in the `default` signature, impose a `Typeable r` constraint. Then we can do a runtime type test to figure out the representation and to squash the levity polymorphism. (This actually works.) A sufficiently smart compiler would be able to optimize away the runtime type test in any non-levity-polymorphic class instance. And we're just left with happiness and a wicked powerful type system. My (rushed, somewhat shoddy) work on this is [https://github.com/goldfirere/ghc/tree/lev-poly-base here]. I don't expect that to ever be merged -- I just was exploring the possibility. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:29 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12980 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: Old description:
I can create a GHC proposal for this but I need a sanity check first
{{{#!hs import Prelude hiding (Num (..)) import qualified Prelude as P import GHC.Prim import GHC.Types
class Num (a :: TYPE k) where (+) :: a -> a -> a (-) :: a -> a -> a (*) :: a -> a -> a negate :: a -> a abs :: a -> a signum :: a -> a
fromInteger :: Integer -> a
instance Num Int# where (+) :: Int# -> Int# -> Int# (+) = (+#)
(-) :: Int# -> Int# -> Int# (-) = (-#)
(*) :: Int# -> Int# -> Int# (*) = (*#)
negate :: Int# -> Int# negate = negateInt#
...
fromInteger :: Integer -> Int# fromInteger (fromInteger @PtrRepLifted @Int -> I# int) = int
instance Num Double# where (+) :: Double# -> Double# -> Double# (+) = (+##)
(-) :: Double# -> Double# -> Double# (-) = (-##)
(*) :: Double# -> Double# -> Double# (*) = (*##)
negate :: Double# -> Double# negate = negateDouble#
...
fromInteger :: Integer -> Double# fromInteger (fromInteger @PtrRepLifted @Double -> D# dbl) = dbl }}}
Note how the `fromInteger` views aren't qualified? That's because we can branch on the kind and all of a sudden, all instances of old `Num` are instances of our `Num`
{{{#!hs instance P.Num a => Num (a :: Type) where (+) = (P.+) @a (-) = (P.-) @a (*) = (P.*) @a negate = P.negate @a abs = P.abs @a signum = P.signum @a fromInteger = P.fromInteger @a }}}
----
Same with `Show` etc. etc.
{{{#!hs class Show (a :: TYPE k) where show :: (a :: TYPE k) -> String
instance P.Show a => Show (a :: Type) where show :: (a :: Type) -> String show = P.show @a
instance Show (Int# :: TYPE IntRep) where show :: Int# -> String show int = show @PtrRepLifted @Int (I# int)
instance Show (Double# :: TYPE DoubleRep) where show :: Double# -> String show dbl = show @PtrRepLifted @Double (D# dbl) }}}
{{{#!hs class Functor (f :: Type -> TYPE rep) where fmap :: (a -> b) -> (f a -> f b)
instance Functor ((# , #) a) where fmap :: (b -> b') -> ((# a, b #) -> (# a, b' #)) fmap f (# a, b #) = (# a, f b #)
class Applicative (f :: Type -> TYPE rep) where pure :: a -> f a (<*>) :: f (a -> b) -> (f a -> f b)
instance Monoid m => Applicative ((# , #) m) where pure :: a -> (# m, a #) pure a = (# mempty, a #)
(<*>) :: (# m, a -> b #) -> ((# m, a #) -> (# m, b #)) (# m1, f #) <*> (# m2, x #) = (# m1 <> m2, f x #)
class Foldable (f :: Type -> TYPE rep) where fold :: Monoid m => f m -> m
instance Foldable ((# , #) xx) where fold :: Monoid m => (# xx, m #) -> m fold (# _, m #) = m }}}
halp where does this end
----
What effects would this have? They are even printed the same by default
{{{#!hs Prelude.Num :: * -> Constraint Main.Num :: * -> Constraint
-- >>> :set -fprint-explicit-runtime-reps Prelude.Num :: * -> Constraint Main.Num :: TYPE k -> Constraint
-- >>> :set -fprint-explicit-foralls Prelude.Num :: * -> Constraint Main.Num :: forall (k :: RuntimeRep). TYPE k -> Constraint }}}
New description: **See ghc-proposal**: [https://github.com/ghc-proposals/ghc- proposals/pull/30 Levity-Polymorphic Type Classes] ---- I can create a GHC proposal for this but I need a sanity check first {{{#!hs import Prelude hiding (Num (..)) import qualified Prelude as P import GHC.Prim import GHC.Types class Num (a :: TYPE k) where (+) :: a -> a -> a (-) :: a -> a -> a (*) :: a -> a -> a negate :: a -> a abs :: a -> a signum :: a -> a fromInteger :: Integer -> a instance Num Int# where (+) :: Int# -> Int# -> Int# (+) = (+#) (-) :: Int# -> Int# -> Int# (-) = (-#) (*) :: Int# -> Int# -> Int# (*) = (*#) negate :: Int# -> Int# negate = negateInt# ... fromInteger :: Integer -> Int# fromInteger (fromInteger @PtrRepLifted @Int -> I# int) = int instance Num Double# where (+) :: Double# -> Double# -> Double# (+) = (+##) (-) :: Double# -> Double# -> Double# (-) = (-##) (*) :: Double# -> Double# -> Double# (*) = (*##) negate :: Double# -> Double# negate = negateDouble# ... fromInteger :: Integer -> Double# fromInteger (fromInteger @PtrRepLifted @Double -> D# dbl) = dbl }}} Note how the `fromInteger` views aren't qualified? That's because we can branch on the kind and all of a sudden, all instances of old `Num` are instances of our `Num` {{{#!hs instance P.Num a => Num (a :: Type) where (+) = (P.+) @a (-) = (P.-) @a (*) = (P.*) @a negate = P.negate @a abs = P.abs @a signum = P.signum @a fromInteger = P.fromInteger @a }}} ---- Same with `Show` etc. etc. {{{#!hs class Show (a :: TYPE k) where show :: (a :: TYPE k) -> String instance P.Show a => Show (a :: Type) where show :: (a :: Type) -> String show = P.show @a instance Show (Int# :: TYPE IntRep) where show :: Int# -> String show int = show @PtrRepLifted @Int (I# int) instance Show (Double# :: TYPE DoubleRep) where show :: Double# -> String show dbl = show @PtrRepLifted @Double (D# dbl) }}} {{{#!hs class Functor (f :: Type -> TYPE rep) where fmap :: (a -> b) -> (f a -> f b) instance Functor ((# , #) a) where fmap :: (b -> b') -> ((# a, b #) -> (# a, b' #)) fmap f (# a, b #) = (# a, f b #) class Applicative (f :: Type -> TYPE rep) where pure :: a -> f a (<*>) :: f (a -> b) -> (f a -> f b) instance Monoid m => Applicative ((# , #) m) where pure :: a -> (# m, a #) pure a = (# mempty, a #) (<*>) :: (# m, a -> b #) -> ((# m, a #) -> (# m, b #)) (# m1, f #) <*> (# m2, x #) = (# m1 <> m2, f x #) class Foldable (f :: Type -> TYPE rep) where fold :: Monoid m => f m -> m instance Foldable ((# , #) xx) where fold :: Monoid m => (# xx, m #) -> m fold (# _, m #) = m }}} halp where does this end ---- What effects would this have? They are even printed the same by default {{{#!hs Prelude.Num :: * -> Constraint Main.Num :: * -> Constraint -- >>> :set -fprint-explicit-runtime-reps Prelude.Num :: * -> Constraint Main.Num :: TYPE k -> Constraint -- >>> :set -fprint-explicit-foralls Prelude.Num :: * -> Constraint Main.Num :: forall (k :: RuntimeRep). TYPE k -> Constraint }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:30 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12708: RFC: Representation polymorphic Num -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Core Libraries | Version: 8.0.1 Resolution: | Keywords: | LevityPolymorphism Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12980 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by vagarenko): * cc: vagarenko (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12708#comment:31 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC