Opened 3 years ago

Last modified 2 years ago

#12708 new feature request

RFC: Representation polymorphic Num — at Version 8

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Core Libraries Version: 8.0.1
Keywords: LevityPolymorphism Cc: ekmett, oerjan, vagarenko
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 (last modified by Iceland_jack)

I can create a GHC proposal for this but I need a sanity check first

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

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.

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)
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

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

Change History (8)

comment:1 Changed 3 years ago 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)

--   × × × 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)

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?

UU.fromInteger :: Prelude.Num  a => Integer -> a
(UU.+)         :: Prelude.Num  a => a -> a -> a
(UU.show)      :: Prelude.Show a => a -> String

)

Edit: Applying IntRep gets us from Prelude.Show to UU.Show:

UU.show         :: Prelude.Show a => a -> String
UU.show @IntRep ::      UU.Show a => a -> String -- where (a :: TYPE 'IntRep)

Edit 2: It also seems like the non Type instances don't show up in :info Num, :info Eq, ....

Last edited 3 years ago by Iceland_jack (previous) (diff)

comment:2 Changed 3 years ago by Iceland_jack

With it and RebindableSyntax you can write

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

class Eq (a :: TYPE rep) where
  (==) :: a -> a -> Bool

instance Eq (Int# :: TYPE IntRep) where
  (==) :: Int# -> Int# -> Bool
  a == b = isTrue# (a ==# b)

instance Eq (Addr# :: TYPE AddrRep) where
  (==) :: Addr# -> Addr# -> Bool
  a == b = isTrue# (eqAddr# a b) 

is5 :: Int# -> Bool
is5 5 = True
is5 _ = False

class Eq a => Ord (a :: TYPE rep) where
  (<) :: a -> a -> Bool

instance Ord (Int# :: TYPE IntRep) where
  a < b = isTrue# (a <# b)

Enjoy the possibility of rep polymorphic Bits, maybe even Semigroup, Monoid...

((any idea why

class Eq (a :: TYPE rep) where
  (==) :: a -> a -> Bool
  (==) = undefined

is fine but

-- UU.hs:105:3: error: …
--     A representation-polymorphic type is not allowed here:
--       Type: a
--       Kind: TYPE k
--     In the type of binder ‘a’
-- Compilation failed.

class Eq (a :: TYPE rep) where
  (==) :: a -> a -> Bool
  a == b = undefined

))

Last edited 3 years ago by Iceland_jack (previous) (diff)

comment:3 Changed 3 years ago by Iceland_jack

Should this not be allowed when minBound :: () -> a is allowed?

class Bounded (TYPE rep) where
  minBound :: a
  minBound :: a

for

instance Bounded Int# where
  minBound :: Int#
  minBound = -9223372036854775808#

  maxBound :: Int#
  maxBound = 9223372036854775807#

comment:4 Changed 3 years ago by Iceland_jack

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)

Edit: It's funny that the unboxed tuples have the complete "HList", sometimes emulated (see Only) but unboxed tuples tho: (##), (# a #), (# a, b #), ...

instance Eq ((##) :: TYPE VoidRep) where
  type Logic (##) = Int#
  (==) :: (##) -> (##) -> Int#
  (##) == (##) = True#

  (/=) :: (##) -> (##) -> Int#
  (##) /= (##) = False#

-- I can't type these?? (see #12094)
-- pattern False# :: Int#
-- pattern True#  :: Int#
pattern False# = 0#
pattern True#  = 1#

Edit 2: Is there no way to refer to (# a #) with prefix application: (# #) a? How am I supposed to make this a Functor yall :)

instance Eq a => Eq ((# a #) :: TYPE UnboxedTupleRep) where
  type Logic (# a #) = Int#
  (==) :: (# a #) -> (# a #) -> Int#
  (# a #) == (# a' #)
    | a == a'   = True#
    | otherwise = False#

  (/=) :: (# a #) -> (# a #) -> Int#
  (# a #) /= (# a' #) 
    | a /= a'   = True#
    | otherwise = False#
instance (Eq a, Eq b) => Eq ((# a, b #) :: TYPE UnboxedTupleRep) where
  (==) :: (# a, b #) -> (# a, b #) -> Bool
  (# a, b #) == (# a', b' #) = and
    [ a == a'
    , b == b' ]

instance (Eq a, Eq b, Eq c) => Eq ((# a, b, c #) :: TYPE UnboxedTupleRep) where
  (==) :: (# a, b, c #) -> (# a, b, c #) -> Bool
  (# a, b, c #) == (# a', b', c' #) = and
    [ a == a'
    , b == b'
    , c == c' ]

instance (Eq a, Eq b, Eq c, Eq d) => Eq ((# a, b, c, d #) :: TYPE UnboxedTupleRep) where
  (==) :: (# a, b, c, d #) -> (# a, b, c, d #) -> Bool
  (# a, b, c, d #) == (# a', b', c', d' #) = and
    [ a == a'
    , b == b'
    , c == c'
    , d == d' ]

class Eq1 (f :: TYPE rep1 -> TYPE rep2) where
  liftEq :: (a -> a' -> Bool) -> (f a -> f a' -> Bool)

instance Eq a => Eq1 ((# , #) a) where
  liftEq :: (b -> b' -> Bool) -> ((# a, b #) -> (# a, b' #) -> Bool)
  liftEq (===) (# a, b #) (# a', b' #) = and
    [ a ==  a'
    , b === b' ]
class Read (a :: TYPE rep) where
  read :: String -> a

instance Read (Int# :: TYPE IntRep) where
  read :: String -> Int#
  read "0#" = 0
  read "1#" = 1
  ...
Last edited 3 years ago by Iceland_jack (previous) (diff)

comment:5 Changed 3 years ago by Iceland_jack

Description: modified (diff)

comment:6 Changed 3 years ago by Iceland_jack

Description: modified (diff)

comment:7 Changed 3 years ago by Iceland_jack

Description: modified (diff)

comment:8 Changed 3 years ago by Iceland_jack

Description: modified (diff)
Note: See TracTickets for help on using tickets.