Re: Why aren't classes like "Num" levity polymorphic?

Another, weaker version of this is to just require default signatures that assume r has type LiftedRep for each of the defaults, but then instantiating things at obscure kinds becomes _much_ harder. -Edward On Mon, May 9, 2022 at 12:30 PM Edward Kmett wrote:

Also, if you do want to experiment with this in ghci you need to set some flags in .ghci:

-- ghci binds 'it' to the last expression by default, but it assumes it lives in Type. this blocks overloaded printing :set -fno-it

-- replace System.IO.print with whatever 'print' is in scope. You'll need a RuntimeRep polymorphic 'print' function, though. :set -interactive-print print

-- we don't want standard Prelude definitions. The above Lev trick for ifThenElse was required because turning on RebindableSyntax broke if. :set -XRebindableSyntax -XNoImplicitPrelude

etc.

With that you can get surprisingly far. It is rather nice being able to use (+) and a Show and the like on primitive Int#s and what have you.

For me the main win is that I can do things like install Eq on (MutableByteArray# s) and the like and stop having to use random function names to access that functionality.

You can also use the new UnliftedDataTypes and/or UnliftedNewtypes to do things like pass around a Natural# that is stored in a couple of registers and then build support for it. This is also included in that repo above.

-Edward

On Mon, May 9, 2022 at 12:24 PM Edward Kmett wrote:

...

It is rather shockingly difficult to get it to work out because of the default definitions in each class.

Consider just

class Eq (a :: TYPE r) where (==), (/=) :: a -> a -> Bool

That looks good until you remember that

x == y = not (x /= y) x /= y = not (x == y)

are also included in the class, and cannot be written in a RuntimeRep polymorphic form!

The problem is that x has unknown rep and is an argument. We can only be levity polymorphic in results.

So you then have to do something like

default (==) :: EqRep r => a -> a -> Bool (==) = eqDef default (/=) :: EqRep r => a -> a -> Bool (/=) = neDef

class EqRep (r :: RuntimeRep) where eqDef, neDef :: forall (a :: TYPE r). Eq a => a -> a -> Bool

and then bury them in a class that actually knows about the RuntimeRep.

We can lift the Prelude.Eq into the modified Eq above pointwise inside kind Type.

instance Prelude.Eq a => Eq (a :: Type) where (==) = (Prelude.==) (/=) = (Prelude./=)

and/or we can instantiate EqRep at _all_ the RuntimeReps.

That is where we run into a problem. You could use a compiler plugin to discharge the constraint (which is something I'm actively looking into) or you can do something like write out a few hand-written instances that are all completely syntactically equal:

instance EqRep LiftedRep where eqDef x y = not (x /= y) neDef x y = not (x == y)

instance EqRep ... where ...

The approach I'm taking today is to use backpack to generate these EqRep instances in a canonical location. It unfortunately breaks GHC when used in sufficient anger to handle TupleRep's of degree 2 in full generality, because command line lengths for each GHC invocation starts crossing 2 megabytes(!) and we break operating system limits on command line lengths, because we don't have full support for passing arguments in files from cabal to ghc.

The approach I'd like to take in the future is to discharge those obligations via plugin.

There are more tricks that you wind up needing when you go to progress to handle things like Functor in a polymorphic enough way.

type Lev (a :: TYPE r) = () => a

is another very useful tool in this toolbox, because it is needed when you want to delay a computation on an argument in a runtime-rep polymorphic way.

Why? Even though a has kind TYPE r. Lev a always has kind Type!

So I can pass it in argument position independent of RuntimeRep.

ifThenElse :: forall r (a :: TYPE r). Bool -> Lev a -> Lev a -> a ifThenElse True x _ = x ifThenElse False _ y = y

Note this function didn't need any fancy FooRep machinery and it has the right semantics in that it doesn't evaluate the arguments prematurely! This trick is needed when you want to go convert some kind of RuntimeRep polymorphic Maybe or List for one RuntimeRep to one for another RuntimeRep unless you want to deal with an explosive number of instances parameterized on pairs of RuntimeReps.

https://github.com/ekmett/unboxed is a repo of me experimenting with this from last year some time.

I'm also giving a talk at Yow! LambdaJam in a week or so on this!

-Edward

On Mon, May 9, 2022 at 11:27 AM Clinton Mead wrote:

...

Hi All

It seems to me to be a free win just to replace:

`class Num a where`

with

`class Num (a :: (r :: RuntimeRep)) where`

And then one could define `Num` instances for unlifted types.

This would make it possible to avoid using the ugly `+#` etc syntax for operations on unlifted types.

`Int#` and `Word#` could have `Num` instances defined just as `Int` and `Word` already have.

I presume there's a reason why this hasn't been done, but I was wondering why?

Thanks, Clinton _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users