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

[Edward Kmett]

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 <ekmett at gmail.com> 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 <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/3d7752d9/attachment.html>