Exposed # kinded variables + polykinded Prelude classes?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

Exposed # kinded variables + polykinded Prelude classes?

Zemyla

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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Exposed # kinded variables + polykinded Prelude classes?

chessai .
Just realised i hit reply and not reply all. Here was my email:


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.

On Sun, Oct 27, 2019, 9:47 AM Zemyla <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: 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 . <[hidden email]> wrote:
Just realised i hit reply and not reply all. Here was my email:


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.

On Sun, Oct 27, 2019, 9:47 AM Zemyla <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Exposed # kinded variables + polykinded Prelude classes?

Richard Eisenberg-5
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 . <[hidden email]> 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 . <[hidden email]> wrote:
Just realised i hit reply and not reply all. Here was my email:


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.

On Sun, Oct 27, 2019, 9:47 AM Zemyla <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries


_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Exposed # kinded variables + polykinded Prelude classes?

Carter Schonwald
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 <[hidden email]> 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 . <[hidden email]> 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 . <[hidden email]> wrote:
Just realised i hit reply and not reply all. Here was my email:


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.

On Sun, Oct 27, 2019, 9:47 AM Zemyla <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

Re: Exposed # kinded variables + polykinded Prelude classes?

John Ericson-2

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 <[hidden email]> 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 . <[hidden email]> 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 . <[hidden email]> wrote:
Just realised i hit reply and not reply all. Here was my email:


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.

On Sun, Oct 27, 2019, 9:47 AM Zemyla <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries