New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Levity-Polymorphic Type Classes #30

Closed
wants to merge 4 commits into
base: master
from

Conversation

Projects
None yet
6 participants
@Icelandjack
Contributor

Icelandjack commented Dec 10, 2016

Original Trac ticket: #12708.
Reddit submission.

Lets us define instances like Num Int#

{-# Language InstanceSigs #-}

class Num (a :: TYPE rep) where
  (+) :: a -> a -> a
  (*) :: a -> a -> a
  fromInteger :: Integer -> a

instance Prelude.Num n => Num (n :: Type) where
  ...

instance Num Int# where
  (+) :: Int# -> Int# -> Int#
  (+) = (+#)

  (*) :: Int# -> Int# -> Int#
  (*) = (*#)

  fromInteger :: Integer -> Int#
  fromInteger (fromInteger -> I# int#) = int#

instance Num Double# where
  (+) :: Double# -> Double# -> Double#
  (+) = (+##)

  (*) :: Double# -> Double# -> Double#
  (*) = (*##)

  fromInteger :: Integer -> Double#
  fromInteger (fromInteger -> D# dbl#) = dbl#

and

class Show (a :: TYPE rep) where
  show :: a -> String

instance Prelude.Show a => Show (a :: Type) where
  show :: a -> String
  show = Prelude.show

instance Show Int# where
  show :: Int# -> String
  show int# = show (I# int#) ++ "#"

instance Show Double# where
  show :: Double# -> String
  show dbl# = show (D# dbl#) ++ "#"

Rendered.

@Icelandjack

This comment has been minimized.

Show comment
Hide comment
@Icelandjack

Icelandjack Dec 10, 2016

Contributor

@goldfirere this fails with -dcore-lint.

Contributor

Icelandjack commented Dec 10, 2016

@goldfirere this fails with -dcore-lint.

@andrewthad

This comment has been minimized.

Show comment
Hide comment
@andrewthad

andrewthad Dec 10, 2016

Contributor

This is interesting, but without an unlifted data types extension, I don't see a good motivation for doing this. Making Eq and Ord work for Int#, Word#, etc. is the only thing I can see where there is an immediate gain from this. To me, the drawback mentioned in the proposal (causing problems for TypeApplications) seems to outweigh this benefit. So I would say that I am opposed to this change unless there is some certainty that an unlifted data types extension is coming to GHC with it. For me, that would tip the scales, since I would really want to be able to fmap over an unlifted Maybe.

Contributor

andrewthad commented Dec 10, 2016

This is interesting, but without an unlifted data types extension, I don't see a good motivation for doing this. Making Eq and Ord work for Int#, Word#, etc. is the only thing I can see where there is an immediate gain from this. To me, the drawback mentioned in the proposal (causing problems for TypeApplications) seems to outweigh this benefit. So I would say that I am opposed to this change unless there is some certainty that an unlifted data types extension is coming to GHC with it. For me, that would tip the scales, since I would really want to be able to fmap over an unlifted Maybe.

@Icelandjack

This comment has been minimized.

Show comment
Hide comment
@Icelandjack

Icelandjack Dec 10, 2016

Contributor

Interestingly Applicative doesn't work, but

class Functor m => Monoidal (m :: TYPE UnboxedTupleRep -> TYPE rep) where
  unit :: () -> m (##)
  mult :: m a -> m b -> m (# a, b #)

does, it is not possible to go from that to the Applicative interface using the usual route (as it should, since <*> shouldn't be levity polymorphic). (##) and (# a, b #) should have different kinds (fixed by #29).

Contributor

Icelandjack commented Dec 10, 2016

Interestingly Applicative doesn't work, but

class Functor m => Monoidal (m :: TYPE UnboxedTupleRep -> TYPE rep) where
  unit :: () -> m (##)
  mult :: m a -> m b -> m (# a, b #)

does, it is not possible to go from that to the Applicative interface using the usual route (as it should, since <*> shouldn't be levity polymorphic). (##) and (# a, b #) should have different kinds (fixed by #29).

@Icelandjack Icelandjack changed the title from Levity Polymorphic Type Classes to Levity-Polymorphic Type Classes Dec 10, 2016

@Icelandjack

This comment has been minimized.

Show comment
Hide comment
@Icelandjack

Icelandjack Dec 10, 2016

Contributor

Stuff

class Semigroup (s :: TYPE rep) where
  (<>) :: s -> s -> s

instance Semigroup m => Monoid (m :: TYPE rep) where
  mempty :: () -> m

data Const :: Type -> forall rep. TYPE rep -> Type where
  Const :: e -> Const e a 

class Functor (f :: forall rep1. TYPE rep1 -> TYPE rep2) where
  fmap :: (a -> a') -> (f a -> f a')

class Functor f => Applicative (f :: forall rep1. TYPE rep1 -> TYPE rep2) where
  pure  :: a -> f a
  (<*>) :: f (a -> b) -> (f a -> f b)

instance Functor (Const e) where
  fmap :: (a -> a') -> (Const e a -> Const e a')
  fmap _ (Const e) = Const e

instance Monoid m => Applicative (Const m) where
  pure :: a -> Const m a
  pure _ = Const (mempty ())

  (<*>) :: Const m (a -> b) -> (Const m a -> Const m b)
  Const m₁ <*> Const m₂ = Const (m₁ <> m₂)
Contributor

Icelandjack commented Dec 10, 2016

Stuff

class Semigroup (s :: TYPE rep) where
  (<>) :: s -> s -> s

instance Semigroup m => Monoid (m :: TYPE rep) where
  mempty :: () -> m

data Const :: Type -> forall rep. TYPE rep -> Type where
  Const :: e -> Const e a 

class Functor (f :: forall rep1. TYPE rep1 -> TYPE rep2) where
  fmap :: (a -> a') -> (f a -> f a')

class Functor f => Applicative (f :: forall rep1. TYPE rep1 -> TYPE rep2) where
  pure  :: a -> f a
  (<*>) :: f (a -> b) -> (f a -> f b)

instance Functor (Const e) where
  fmap :: (a -> a') -> (Const e a -> Const e a')
  fmap _ (Const e) = Const e

instance Monoid m => Applicative (Const m) where
  pure :: a -> Const m a
  pure _ = Const (mempty ())

  (<*>) :: Const m (a -> b) -> (Const m a -> Const m b)
  Const m₁ <*> Const m₂ = Const (m₁ <> m₂)
@RyanGlScott

This comment has been minimized.

Show comment
Hide comment
@RyanGlScott

RyanGlScott Dec 11, 2016

Contributor

Aside from the fact that this stuff barely works today in GHC HEAD (an issue which will eventually be resolved, I imagine), I feel like I'd need a lot more user testimony about actually using these classes in practice before I can be swayed to change our long-established class hierarchy to accommodate levity polymorphic definitions. For instance, how would many type signatures would stop being inferred because of these changes? What effect does it have on the average readability of error messages?

I'll echo @goldfirere's comments here: I think an important first step is to create a separate library that fully implements all of these ideas so that folks can experiment with it. While the numerous examples you've provided are nice to look at, actually being able to get my hands on something I could tinker with would go a long way in persuading me that this is a good idea.

Contributor

RyanGlScott commented Dec 11, 2016

Aside from the fact that this stuff barely works today in GHC HEAD (an issue which will eventually be resolved, I imagine), I feel like I'd need a lot more user testimony about actually using these classes in practice before I can be swayed to change our long-established class hierarchy to accommodate levity polymorphic definitions. For instance, how would many type signatures would stop being inferred because of these changes? What effect does it have on the average readability of error messages?

I'll echo @goldfirere's comments here: I think an important first step is to create a separate library that fully implements all of these ideas so that folks can experiment with it. While the numerous examples you've provided are nice to look at, actually being able to get my hands on something I could tinker with would go a long way in persuading me that this is a good idea.

@bgamari

This comment has been minimized.

Show comment
Hide comment
@bgamari

bgamari Dec 12, 2016

Contributor

I agree that this may be a bit premature. As mentioned by others, I think we will really want more experience working with levity polymorphic classes (e.g. via an alternative Prelude and RebindableSyntax) before we start generalizing base.

Contributor

bgamari commented Dec 12, 2016

I agree that this may be a bit premature. As mentioned by others, I think we will really want more experience working with levity polymorphic classes (e.g. via an alternative Prelude and RebindableSyntax) before we start generalizing base.

@Icelandjack

This comment has been minimized.

Show comment
Hide comment
@Icelandjack

Icelandjack Dec 12, 2016

Contributor

If I create a library should

class                  Functor     (f :: forall rep1. TYPE rep1 -> TYPE rep)
class Functor     f => Applicative (f :: forall rep1. TYPE rep1 -> TYPE rep2)
class Applicative f => Monad       (f :: forall rep1. TYPE rep1 -> TYPE rep2)

be included for experimenting with and what's a good name? This is the only levity-polymorphic Applicative, Monad I can think of.

Contributor

Icelandjack commented Dec 12, 2016

If I create a library should

class                  Functor     (f :: forall rep1. TYPE rep1 -> TYPE rep)
class Functor     f => Applicative (f :: forall rep1. TYPE rep1 -> TYPE rep2)
class Applicative f => Monad       (f :: forall rep1. TYPE rep1 -> TYPE rep2)

be included for experimenting with and what's a good name? This is the only levity-polymorphic Applicative, Monad I can think of.

@goldfirere

This comment has been minimized.

Show comment
Hide comment
@goldfirere

goldfirere Dec 12, 2016

Contributor

You mention a core-lint error. Is this posted as a bug somewhere?

I actually think that this would not cause problems with type inference. I'd want experience to be sure, but I believe all will be well. In particular, inferred types will still be levity-monomorphic because GHC will never infer levity polymorphism. This means that, with this proposal, if you write

myPlus = (+)

the myPlus would be levity-monomorphic, unlike (+). (This is true even without the monomorphism restriction. Indeed, you can view the levity-monomorphism restriction as a relative of the traditional monomorphism restriction that can never be disabled.)

Contributor

goldfirere commented Dec 12, 2016

You mention a core-lint error. Is this posted as a bug somewhere?

I actually think that this would not cause problems with type inference. I'd want experience to be sure, but I believe all will be well. In particular, inferred types will still be levity-monomorphic because GHC will never infer levity polymorphism. This means that, with this proposal, if you write

myPlus = (+)

the myPlus would be levity-monomorphic, unlike (+). (This is true even without the monomorphism restriction. Indeed, you can view the levity-monomorphism restriction as a relative of the traditional monomorphism restriction that can never be disabled.)

@Icelandjack

This comment has been minimized.

Show comment
Hide comment
@Icelandjack

Icelandjack Dec 15, 2016

Contributor

@goldfirere My Internet situation has been zonky — I made a ticket (#12987). I'm glad inference doesn't seem to be a problem.

If I understand correctly, the most general constructors Functor, Pointed, Applicative, Monad accept are

Functor     :: (TYPE rep-> TYPE rep₂) -> Constraint
Pointed     :: (TYPE rep-> TYPE rep₂) -> Constraint
Applicative :: (Type      -> TYPE rep)  -> Constraint
Monad       :: (Type      -> TYPE rep)  -> Constraint

but if Monad includes join it must be constrained to

Monad :: (Type -> Type) -> Constraint

Is this meaningless or does it have deeper implications? Everyone please share cool levity-polymorphic classes you can think of!

Contributor

Icelandjack commented Dec 15, 2016

@goldfirere My Internet situation has been zonky — I made a ticket (#12987). I'm glad inference doesn't seem to be a problem.

If I understand correctly, the most general constructors Functor, Pointed, Applicative, Monad accept are

Functor     :: (TYPE rep-> TYPE rep₂) -> Constraint
Pointed     :: (TYPE rep-> TYPE rep₂) -> Constraint
Applicative :: (Type      -> TYPE rep)  -> Constraint
Monad       :: (Type      -> TYPE rep)  -> Constraint

but if Monad includes join it must be constrained to

Monad :: (Type -> Type) -> Constraint

Is this meaningless or does it have deeper implications? Everyone please share cool levity-polymorphic classes you can think of!

@bgamari

This comment has been minimized.

Show comment
Hide comment
@bgamari

bgamari Jan 24, 2017

Contributor

Note that this proposal is roughly one week from the end of its four week long discussion period. At the end of this period we ask @Icelandjack to summarize the discussion and bring the proposal to the GHC committee for consideration. Thanks!

Contributor

bgamari commented Jan 24, 2017

Note that this proposal is roughly one week from the end of its four week long discussion period. At the end of this period we ask @Icelandjack to summarize the discussion and bring the proposal to the GHC committee for consideration. Thanks!

@nomeata

This comment has been minimized.

Show comment
Hide comment
@nomeata

nomeata Feb 27, 2017

Contributor

This proposal has not attracted discussion for a while. Please consider submitting it to the Committee for discussion, if you think it is ready, or close it, if you have abandoned this proposal.

Contributor

nomeata commented Feb 27, 2017

This proposal has not attracted discussion for a while. Please consider submitting it to the Committee for discussion, if you think it is ready, or close it, if you have abandoned this proposal.

@nomeata

This comment has been minimized.

Show comment
Hide comment
@nomeata

nomeata Apr 13, 2017

Contributor

Another ping. @Icelandjack, whither this proposal?

Contributor

nomeata commented Apr 13, 2017

Another ping. @Icelandjack, whither this proposal?

@nomeata

This comment has been minimized.

Show comment
Hide comment
@nomeata

nomeata May 7, 2017

Contributor

Due to lack of activity, I am marking this proposal as dormant.

Contributor

nomeata commented May 7, 2017

Due to lack of activity, I am marking this proposal as dormant.

@nomeata nomeata added the dormant label May 7, 2017

@nomeata

This comment has been minimized.

Show comment
Hide comment
@nomeata

nomeata Feb 23, 2018

Contributor

This has been dormant for a long time. @Icelandjack, is this abandonned? In that case, please consider closing it.

Contributor

nomeata commented Feb 23, 2018

This has been dormant for a long time. @Icelandjack, is this abandonned? In that case, please consider closing it.

@nomeata

This comment has been minimized.

Show comment
Hide comment
@nomeata

nomeata Apr 9, 2018

Contributor

Closing due to inactivity, but it can of course be reactivated any time.

Contributor

nomeata commented Apr 9, 2018

Closing due to inactivity, but it can of course be reactivated any time.

@nomeata nomeata closed this Apr 9, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment