[GHC] #12708: RFC: Representation polymorphic Num

[GHC]

#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