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

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

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