Re: [GHC] #12708: RFC: Representation polymorphic Num

6 Dec 2016


      #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

    