Opened 3 years ago

Last modified 2 years ago

## #12708 new feature request

# RFC: Representation polymorphic Num — at Version 18

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 )

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

### Change History (18)

### comment:2 Changed 3 years ago by

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

))

### comment:3 follow-up: 11 Changed 3 years ago by

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

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

### comment:5 Changed 3 years ago by

Description: | modified (diff) |
---|

### comment:6 Changed 3 years ago by

Description: | modified (diff) |
---|

### comment:7 Changed 3 years ago by

Description: | modified (diff) |
---|

### comment:8 Changed 3 years ago by

Description: | modified (diff) |
---|

### comment:9 Changed 3 years ago by

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

### comment:11 Changed 3 years ago by

Replying to Iceland_jack:

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

By gum, this is brilliant.

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

### comment:13 Changed 3 years ago by

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#

### comment:14 Changed 3 years ago by

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

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

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

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

### comment:18 Changed 3 years ago by

Description: | modified (diff) |
---|

**Note:**See TracTickets for help on using tickets.

(I am concerned that it seems the instance resolution defaults to

`Type`

.. if I remove the instances (and qualify the`fromInteger`

views)the types of

`show`

and`(+)`

are (let's give it a module name`UU`

)whereas with those instances it seems to default to the

`Type`

, is this intended?)

Edit: Applying`IntRep`

gets us from`Prelude.Show`

to`UU.Show`

:Edit 2: It also seems like the non`Type`

instances don't show up in`:info Num`

,`:info Eq`

, ....