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

[Edward Kmett]

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