RFC: Representation polymorphic Num

[Iceland_jack]

See ghc-proposal: ​Levity-Polymorphic Type Classes

---

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

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

[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

))

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

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

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

[goldfire]

By gum, this is brilliant.

[goldfire]

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.

[nomeata]

By gum, this is brilliant.

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

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

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

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

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

[bgamari]

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

[Iceland_jack]

Using the generalized function composition from the paper

(·) :: forall (r :: RuntimeRep) (a :: Type) (b :: Type) (c :: TYPE r).
      (b -> c) -> (a -> b) -> (a -> c)
(f · g) x = f (g x)

we can write

  fromInteger (fromInteger -> I# i) = i
  fromInteger (fromInteger -> D# d) = d

pointfree

  fromInteger :: Integer -> Int#
  fromInteger = getInt# · fromInteger where
    getInt# :: Int -> Int#
    getInt# (I# i) = i

  fromInteger :: Integer -> Double#
  fromInteger = getDouble# · fromInteger where
    getDouble# :: Double -> Double#
    getDouble# (D# d) = d

[goldfire]

I still believe this is a great idea and would welcome a formal proposal about this. I also still believe that this is something better done in a library for a release or so before we start mucking with something so fundamental. There's nothing about this that cannot be done in a library (modulo RebindableSyntax).

[Iceland_jack]

Replying to goldfire:

I still believe this is a great idea and would welcome a formal proposal about this.

​Done.

[carter]

Replying to goldfire:

I still believe this is a great idea and would welcome a formal proposal about this. I also still believe that this is something better done in a library for a release or so before we start mucking with something so fundamental. There's nothing about this that cannot be done in a library (modulo RebindableSyntax).

I agree with richard, experimental changes to the core num prelude, especially those using still new constructs should happen in userland first.

[oerjan]

Replying to goldfire:

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.

The question is, how would you store the necessary Int# in the dictionary? It seems to me you'd have to use some kind of indirection because otherwise you have a dictionary field than can have arbitrary size.

[goldfire]

Replying to oerjan:

The question is, how would you store the necessary Int# in the dictionary? It seems to me you'd have to use some kind of indirection because otherwise you have a dictionary field than can have arbitrary size.

Spot on. You're right -- we would have a problem with Bounded.

[goldfire]

An exhaustive search through ghc-prim and base found 34 (!) classes that can be generalized this way:

Eq, Ord, Functor, Applicative, Monad, MonadFail, MonadFix, MonadIO,
Bifoldable, Bifunctor, HasResolution, Foldable, Eq1, Ord1, Eq2, Ord2,
IsString, TestCoercion, TestEquality, Storable, IsList, Num, Real,
Fractional, Generic, Generic1, GHCiSandboxIO, BufferedIO, RawIO,
IsLabel, PrintfType, HPrintfType, PrintfArg, IsChar

Some are surely more useful to generalize than others. But wow!

More classes morally could be included in this list but for two limiting factors:

• Many classes use lists somewhere. (For example, Show.) However, we could define a family of list types, one for each representation (which would box unboxed tuples), and then use a type family to select the appropriate list type, allowing generalizations of classes that use lists.
• Several classes (e.g., Integral) use tuples, preventing generalization. But we could just use unboxed tuples and away we go.

Another annoyance was that Applicative can be generalized to make its parameter f :: Type -> TYPE r, but not f :: TYPE r1 -> TYPE r2. The latter is impossible because the class definition mentions f (a -> b), and functions are always lifted.

It would be lovely, though, to ponder the possibility of class Applicative (f :: forall (r1 :: RuntimeRep). TYPE r1 -> TYPE r2), where Applicative would then have a higher-rank kind. And, we could generalize IO (it's implemented using an unboxed tuple, after all) and then IO could be made an instance of this new Applicative. Monad would soon follow, and you'd then be able to return unboxed values in do-notation.

A final note: In testing all this, I had to add default signatures imposing a r ~ LiftedRep constraint whenever a generalized class had a default implementation, because the default implementation would work only at kind Type. This works, but it's disappointing that there can be no defaults at representations other than LiftedRep. However, I've realized we can. Instead of r ~ LiftedRep in the default signature, impose a Typeable r constraint. Then we can do a runtime type test to figure out the representation and to squash the levity polymorphism. (This actually works.) A sufficiently smart compiler would be able to optimize away the runtime type test in any non-levity-polymorphic class instance. And we're just left with happiness and a wicked powerful type system.

My (rushed, somewhat shoddy) work on this is ​here. I don't expect that to ever be merged -- I just was exploring the possibility.