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

[Edward Kmett]

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 <clintonmead at gmail.com> 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20220509/fa64fa0f/attachment.html>