Opened 3 years ago

# RFC: Representation polymorphic Num — at Version 8

Reported by: Owned by: Iceland_jack normal Core Libraries 8.0.1 LevityPolymorphism ekmett, oerjan, vagarenko Unknown/Multiple Unknown/Multiple None/Unknown

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

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

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

instance Read (Int# :: TYPE IntRep) where
...
```
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.