Opened 3 years ago
Last modified 2 years ago
#12708 new feature request
RFC: Representation polymorphic Num
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: | #12980 | Differential Rev(s): | |
Wiki Page: |
Description (last modified by )
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
Change History (31)
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 follow-up: 25 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
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) |
---|
comment:19 Changed 3 years ago by
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
comment:20 Changed 3 years ago by
Keywords: | LevityPolymorphism added |
---|
comment:21 Changed 3 years ago by
Description: | modified (diff) |
---|
comment:22 follow-ups: 23 24 Changed 3 years ago by
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
).
comment:23 Changed 3 years ago by
comment:24 Changed 3 years ago by
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.
comment:25 follow-up: 26 Changed 3 years ago by
Cc: | oerjan added |
---|
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, likeminBound
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.
comment:26 Changed 3 years ago by
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
.
comment:27 Changed 3 years ago by
Related Tickets: | → 12980 |
---|
comment:28 Changed 3 years ago by
Related Tickets: | 12980 → #12980 |
---|
comment:29 Changed 3 years ago by
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.
comment:30 Changed 3 years ago by
Description: | modified (diff) |
---|
comment:31 Changed 2 years ago by
Cc: | vagarenko added |
---|
(I am concerned that it seems the instance resolution defaults to
Type
.. if I remove the instances (and qualify thefromInteger
views)the types of
show
and(+)
are (let's give it a module nameUU
)whereas with those instances it seems to default to the
Type
, is this intended?)
Edit: Applying
IntRep
gets us fromPrelude.Show
toUU.Show
:Edit 2: It also seems like the non
Type
instances don't show up in:info Num
,:info Eq
, ....