Opened 3 years ago

# RFC: Representation polymorphic Num — at Version 18

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

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.

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)
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 follow-up:  11 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)

### comment:9 Changed 3 years ago by Iceland_jack

With the upcoming UnboxedSums

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

instance Functor     ((# | #) a)
instance Applicative ((# | #) a)
instance Foldable    ((# | #) a)
...
Last edited 3 years ago by Iceland_jack (previous) (diff)

### comment:10 Changed 3 years ago by goldfire

By gum, this is brilliant.

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

### comment:11 in reply to:  3 Changed 3 years ago by goldfire

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.

### comment:12 Changed 3 years ago by nomeata

By gum, this is brilliant.

He wanted a sanity check, not a brilliance check :-)

### comment:13 Changed 3 years ago by Iceland_jack

If we did like subhask we could even interpret == in a different logic

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

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

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

Edit: Is there any potential for run-time polymorphism here?

instance Eq b => Eq (a -> b) where
type Logic (a -> b) = a -> Logic b
(==) :: (a -> b) -> (a -> b) -> (a -> Logic b)
(f == g) x = f x == g x

Edit 2: This is more restrictive than eqStableName# :: StableName# a -> StableName# b -> Int#

instance Eq (StableName# a :: TYPE PtrRepUnlifted) where
type Logic (StableName# a) = Int#
(==) :: StableName# a -> StableName# a -> Int#
(==) = eqStableName#
Last edited 3 years ago by Iceland_jack (previous) (diff)

### comment:14 Changed 3 years ago 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.

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

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

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:

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

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

### comment:16 Changed 3 years ago by Iceland_jack

This is a pipe dream, Logic offers cool possibilities.

sbv has EqSymbolic which is an Eq a where Logic a ~ SBool :

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)

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.

### comment:17 Changed 3 years ago by bgamari

Simon and Richard's recent PLDI submission on levity polymorphism is quite relevant to this ticket (and in fact cites it).

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

### comment:18 Changed 3 years ago by Iceland_jack

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