haskellari / some

Existential type.
BSD 3-Clause "New" or "Revised" License
36 stars 13 forks source link

GShow is the same as Show1 from base #19

Closed Ericson2314 closed 4 years ago

Ericson2314 commented 4 years ago

Unlike the other classes, there are no proof obligations that matching on the indices can satisfy. It's therefore not a "GADT class" as I understand them.

edit I am wrong, GShow t is not the same as Show1 t it is the same as forall a. Show (t a). Do not, reader, that this holds in general: the Foo1 classes are not completely obviated by quantified constraints.

phadej commented 4 years ago

No the aren't the same.

class Show1 f where
    liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) ->
        Int -> f a -> ShowS

class GShow t where
    gshowsPrec :: -- nothing here
    Int -> t a -> ShowS

As a concrete example take

data SBool (b :: Bool) where
    STrue  :: SBool 'True
    SFalse :: SBool 'False

instance GShow SBool where
    gshowsPrec _ STrue = showString "STrue"
    gshowsPrec _ SFalse = showString "SFalse"

(One can argue it could be named differently, as one can write e.g. GShow Proxy instance, which indeed isn't GADT, but still, GShow isn't Show1; and naming is hard).

Ericson2314 commented 4 years ago

OK I'm sorry they are not exactly the same, I still don't think GShow adds any value.

First of all, you can implement each in terms of the other:

class GShow t => Show1 f where
    liftShowsPrec _ _ = gshowsPrec

class Show1 f => GShow t where
    gshowsPrec = liftShowsPrec (\_ _ -> id) (\_ -> id)

And second of all, Show1 offers more flexibility of the GADT index does in fact relate to the types of a field.

Now one could argue that is a bad thing, in which case I say GShow is obviated by the quantified constraint forall a. Show (t a).

phadej commented 4 years ago

Show1 is not the same, see kinds and SBool example.

The quantified constraint is same however, but uses quantified constraints (GHC-8.6) when GShow works with GHC-7.0.

I don’t understand what is the problem GShow raises, more boilerplate?

On 25. Jan 2020, at 18.55, John Ericson notifications@github.com wrote:

 OK I'm sorry they are not exactly the same, I still don't think GShow adds any value.

First of all, you can implement each in terms of the other:

class GShow t => Show1 f where liftShowsPrec = gshowsPrec

class Show1 f => GShow t where gshowsPrec = liftShowsPrec (_ -> id) (\ -> id) And second of all, Show1 offers more flexibility of the GADT index does in fact relate to the types of a field.

Now one could argue that is a bad thing, in which case I say GShow is obviated by the quantified constraint forall a. Show (t a).

— You are receiving this because you modified the open/close state. Reply to this email directly, view it on GitHub, or unsubscribe.

Ericson2314 commented 4 years ago

The problem is sort of an ecosystem split where some packages might use the quantified constraint and some would use GShow. My second PR just adds a basic default method, which I assume shouldn't be controversial. My third one adds in 8.6 <= the quantified constraint as a superclass to try to heal the ecosystem split: the idea is that you can't forget the show instances anymore of you write GShow, so you won't forget and more crates can work with you.