Exposed # kinded variables + polykinded Prelude classes?
John Ericson
john.ericson at obsidian.systems
Wed Nov 6 21:22:58 UTC 2019
I want to add that there is a bunch of nastiness with fixed-size number
prim types that I, Carter, and Ömer have been dealing with, and I want
to make the /breaking/ change {Int,Word}<N> is always a boxed
{Int,Word}<N>#, for sake of avoiding a painful and pointless CPP soup.
Given all this, I think we should definitely wait. The status quo is de
facto stabilizing (as an nicer export would) to any degree.
John
On 11/5/19 12:53 PM, Carter Schonwald wrote:
> 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
> <mailto: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
>> <mailto: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
>> <mailto: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
>> <mailto: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 <mailto:Libraries at haskell.org>
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>
>> _______________________________________________
>> Libraries mailing list
>> Libraries at haskell.org <mailto:Libraries at haskell.org>
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org <mailto: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/20191106/d1acf27e/attachment.html>
More information about the Libraries
mailing list