Exposed # kinded variables + polykinded Prelude classes?

[chessai .]

Regarding UnliftedNewtypes: apparently GND can solve this issue for you.
There are som cases where, because of the desugaring, a GND clause will
fail, but moving the clause out to a StandaloneDeriving one can fix the
issue.

But defaults still become annoying for things like Foldable, where most
users rely pretty heavily on defaults.

On Sun, Oct 27, 2019, 4:22 PM chessai . <chessai1996 at gmail.com> wrote:

> Just realised i hit reply and not reply all. Here was my email:
>
> See https://github.com/chessai/levity and
> http://hackage.haskell.org/package/unlifted-list.
>
> There are a few annoyances due to binder restrictions (see [1]).
>
> For example, it is not possible to write polymorphic
> `bindUnliftedToLifted`:
>
> ```
> bindUnliftedToLifted :: forall (a :: TYPE r) (b :: TYPE 'LiftedRep). ST s
> a -> (a -> ST s b) -> ST s b
> ```
>
> This function is frequently useful when working with monads which have
> levity-polymorphic parameters, but you cannot write it when a is
> levity-polymorphic, since it will occur in a binding position. What ends up
> happening is that you write monomorphic versions of this function for each
> one you need. Clearly not desirable.
>
> The other thing is that levity-polymorphic kinds are (almost?) never
> inferred. For example, if I have:
>
> ```
> class Show (a :: TYPE r) where
>   show :: a -> String
>
> addNewline :: Show a => a -> String
> addNewline x = show x ++ "\n"
> ```
>
> GHC will infer the kind of `a` in `addNewline` to be `TYPE 'LiftedRep`,
> even though it very well could be `forall (r :: RuntimeRep). TYPE r`. In
> other words, users will have to constantly kind-annotate because of
> (over-?)restrictive inference. This becomes annoying rather quickly, and
> the type errors don't always immediately make it clear what's happening
> when you miss an annotation.
>
> Another thing which is annoying, you can't write things like Monoid or
> Bounded in the same way! (See also [1])
>
> ```
> class Monoid (a :: TYPE r) where
>   mempty :: a
> ```
>
> GHC will complain about mempty here. You have to instead make it
>
> ```
> class Monoid (a :: TYPE r) where
>   mempty :: () -> a
> ```
>
> which just becomes cluttering, your code gets filled with a lot of `mempty
> ()`.
>
> Another thing is that default implementations will not work. You state
> that it's fine because the number of inhabitants of unlifted kinds is small
> and finite. This will not be the case in GHC 8.10, when UnliftedNewtypes
> lands. Then the number of inhabitants becomes non-finite.
>
> The ways to use levity-polymorhism which result in the best UX are: 1)
> CPS, 2) backpack, and 3) resolving [1]. (1) is the easiest to most users
> right now (see [2] for an example)
>
> With all of these drawbacks I'm against having the API of base or any core
> library really be a place for levity-polymorphic code, especially when
> talking about core typeclasses/types. Probably best for this to be in
> userspace.
>
> [1]: https://gitlab.haskell.org/ghc/ghc/issues/14917
> [2]:
> http://hackage.haskell.org/package/bytesmith-0.3.0.0/docs/src/Data.Bytes.Parser.Internal.html#Parser
>
> On Sun, Oct 27, 2019, 9:47 AM Zemyla <zemyla at gmail.com> wrote:
>
>> I'm wondering if there would be a benefit, if not to the average
>> programmer, then to the ones working on deeper/faster code, to allow some
>> of the # kinded types (mostly Int#, Word#, Char#, Float#, Double#) to be
>> used in Safe code, and to have typeclasses able to work with them.
>>
>> For instance, the definition of Show would become:
>>
>> class Show (a :: TYPE r) where
>>   show :: a -> String
>>   default show :: (r ~ 'LiftedRep) => a -> String
>>   show x = showsPrec 0 x ""
>>
>>   showsPrec :: Int -> a -> ShowS
>>   default showsPrec :: (r ~ 'LiftedRep) => Int -> a -> ShowS
>>   showsPrec _ x s = show x ++ s
>>
>>   showList :: (r ~ 'LiftedRep) => [a] -> ShowS
>>   showList ls s = showList__ shows ls s
>>
>> The fact that the defaults only work when the type is a LiftedRep is a
>> nonissue, because there's only a finite number of non-lifted types we'd be
>> defining it for.
>>
>> You could do the same with Eq, Ord, Num, Real, Integral, Fractional,
>> Floating, RealFrac, RealFloat, Semigroup, Monoid, Bits, FiniteBits, and
>> probably several others I can't think of right now. However, with the
>> functions that return pairs, you'd need a version that returns an unboxed
>> pair instead. Assuming you changed ReadPrec, you could even do the same
>> with Read:
>>
>> newtype ReadP (a :: RuntimeRep r) = ReadP (forall b. (a -> R b) -> R b)
>> newtype ReadPrec (a :: RuntimeRep r) = ReadPrec (Int -> ReadP a)
>>
>> IO, ST, and STM could be made polykinded the same way, and would open up
>> Storable. However, how to do a definition for Monad that works for
>> polykinded monads is an issue. I do know that RebindableSyntax handles it
>> easily when there's just one monad that can operate on multiple kinds,
>> though.
>>
>> As for which # types could be exposed, I'm thinking that Char#, Int#,
>> Word#, Float#, Double#, and Proxy# wouldn't be able to break out of Safe
>> code. Int64# and Word64# would work as well, and for 64-bit machines would
>> just be type aliases for Int# and Word# respectively. For types which have
>> functions with undefined behavior for some arguments, you can just make
>> wrappers that check the arguments and error out for the bad values.
>> MutVar#, MVar#, TVar#, and StableName# don't open up any functions that
>> would be unsuitable for safe code, either. I'm pretty sure that Array# and
>> MutableArray# would also be safe, as long as all functions were
>> length-checked and threw errors instead of having undefined behavior.
>>
>> As for why this would be a desirable thing? Mostly for the sake of
>> convenience and generality, I think. I find myself working with unboxed
>> values from time to time, and it's a pain to always remember to use (+#)
>> for Int# and plusWord# for Word#. In addition, having typeclasses that can
>> return unboxed values (like a hypothetical sized# :: Sized a => a -> Int#
>> vs sized :: Sized a => a -> Int) can improve the generated code when the
>> code using the typeclass doesn't get specialized.
>>
>> The module to import these would have to explain the differences between
>> # kinded types and * kinded ones: # values aren't lazy; they can't be
>> top-level definitions; you can't use unboxed tuples or sums with GHCi; and
>> with a few exceptions, you can't place them in containers (you can't have
>> an [Int#], for instance).
>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20191027/c971d885/attachment.html>