Exposed # kinded variables + polykinded Prelude classes?

Tue Nov 5 17:53:50 UTC 2019

i personally think that levity engineering etc in ghc et al is still too
nascent for adding it to prelude/base in type classes to make sense

I also owe richard some notes on a bit of a feature request for ghc that
probably would compliment supporting such an eventual direction, should it
ever make sense!

we now have a mostly firm foundation for describing semantics for all the
"primmitive" types the rts needs to know about, but that doesnt really
address whether or not that should be a user visible concern, let alone the
user impact/utility of exposing that knob in widely used classes

On Mon, Oct 28, 2019 at 7:02 AM Richard Eisenberg <rae at richarde.dev> wrote:

> There are two things at play here: 1) Safe Haskell, and 2)
> levity-polymorphic classes.
>
> I think (1) is straightforward. I can't think of any lack of safety or
> loss of abstraction from levity polymorphism, and now that the issue has
> been raised, I think the lack of Safe Haskell support for levity
> polymorphism is a bug. Would you want to file a ticket?
>
> I think (2) is quite possible, but with design issues (of course). This
> has actually been discussed before:
> https://github.com/ghc-proposals/ghc-proposals/pull/30  Note that the
> proposal withered on the vine due to lack of love, but it had some support
> -- it was not rejected. As I've posted previously, I think the right way to
> get this is to make an alternative, levity-plymorphic prelude, just to see
> how it all works out. But I do like this direction of travel.
>
> Richard
>
> On Oct 27, 2019, at 9:47 PM, chessai . <chessai1996 at gmail.com> wrote:
>
> 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
>>>
>> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
>
> _______________________________________________
> 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/20191105/42d62094/attachment.html>