Re: default roles

[Richard Eisenberg]

Please see below.

On Oct 10, 2013, at 10:09 PM, Edward Kmett wrote:

> Wait, that sounds like it induces bad semantics. 
> 
> Can't we use that as yet another way to attack the sanctity of Set?
> 
> class Ord a => Foo a where
>   badInsert :: a -> Set a -> Set a
> 
> instance Foo Int where
>   badInsert = insert
> 
> newtype Bar = Bar Int deriving (Eq,Foo)
> 
> instance Ord Bar where
>   compare (Bar x) (Bar y) = compare y x
> 
> Now you can badInsert into a Set.
> 
> If that is still in play then even with all the roles machinery then GND 
> doesn't pass the restrictions of "SafeHaskell". =(

Hrm. Yes.

I'm out of fresh ideas at the moment.

Maybe some will arrive with sleep.

Richard

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: default roles

[Edward Kmett]

Wait, that sounds like it induces bad semantics.

Can't we use that as yet another way to attack the sanctity of Set?

class Ord a => Foo a where
  badInsert :: a -> Set a -> Set a

instance Foo Int where
  badInsert = insert

newtype Bar = Bar Int deriving (Eq,Foo)

instance Ord Bar where
  compare (Bar x) (Bar y) = compare y x

Now you can badInsert into a Set.

If that is still in play then even with all the roles machinery then GND
doesn't pass the restrictions of "SafeHaskell". =(

-Edward


On Thu, Oct 10, 2013 at 9:52 PM, Richard Eisenberg wrote:

>
> On Oct 10, 2013, at 1:14 PM, David Menendez wrote:
> > Sure, but if op uses show internally, we get Int's show, not Age's,
> right? That seems correct, in that it's doing what GND is supposed to do,
> but I'll bet it will surprise people.
>
> Yes, you're right. If a method in a subclass uses a superclass method, it
> uses the base type's instance's method, not the newtype's. Very weird, but
> I guess it makes sense in its own way. This does show how GND can create
> instance incoherence even without storing dictionaries in datatypes.
>
> Richard
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: default roles

[Richard Eisenberg]

On Oct 10, 2013, at 1:14 PM, David Menendez wrote:
> Sure, but if op uses show internally, we get Int's show, not Age's, right? 
> That seems correct, in that it's doing what GND is supposed to do, but I'll 
> bet it will surprise people.

Yes, you're right. If a method in a subclass uses a superclass method, it uses 
the base type's instance's method, not the newtype's. Very weird, but I guess 
it makes sense in its own way. This does show how GND can create instance 
incoherence even without storing dictionaries in datatypes.

Richard

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: default roles

[David Menendez]

On Thu, Oct 10, 2013 at 12:11 PM, Simon Peyton-Jones
wrote:

>  Does GND make sense in cases where the superclasses aren't also derived?
> If I had a type T whose Ord instance made use of the Eq instance for some
> reason, and then I made a newtype T' with a new Eq instance and a GND Ord
> instance, the calls to (==) in the Ord instance will refer to the T
> implementation, right?
>
> ** **
>
> Yes, absolutely. 
>
>   class Show a => C a where
>
> op :: a -> a
>
> ** **
>
> You might want to use GND for the (C Age) instance, but NOT use GND for
> the Show instance.
>

Sure, but if op uses show internally, we get Int's show, not Age's, right?
That seems correct, in that it's doing what GND is supposed to do, but I'll
bet it will surprise people.

-- 
Dave Menendez 

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

RE: default roles

[Simon Peyton-Jones]

Does GND make sense in cases where the superclasses aren't also derived? If I 
had a type T whose Ord instance made use of the Eq instance for some reason, 
and then I made a newtype T' with a new Eq instance and a GND Ord instance, the 
calls to (==) in the Ord instance will refer to the T implementation, right?

Yes, absolutely.
  class Show a => C a where
op :: a -> a

You might want to use GND for the (C Age) instance, but NOT use GND for the 
Show instance.

Simon

From: Glasgow-haskell-users [mailto:glasgow-haskell-users-boun...@haskell.org] 
On Behalf Of David Menendez
Sent: 10 October 2013 16:25
To: Richard Eisenberg
Cc: glasgow-haskell-users@haskell.org Mailing List; Simon Peyton-Jones
Subject: Re: default roles

On Wed, Oct 9, 2013 at 3:21 PM, Richard Eisenberg 
mailto:e...@cis.upenn.edu>> wrote:
Now I think we're on the same page, and I *am* a little worried about the sky 
falling because of this. (That's not a euphemism -- I'm only a little worried.)

Well, maybe I should be more worried.

The whole idea of roles is to protect against type-unsoundness. They are doing 
a great job of that here -- no problem that we've discussed in this thread is a 
threat against type safety.

The issue immediately at hand is about coherence (or perhaps you call it 
confluence) of instances. Roles do not address the issue of coherence at all, 
and thus they fail to protect against coherence attacks. It would take More 
Thought to reformulate roles (or devise something else) to handle coherence.

It's worth pointing out that this isn't a new problem, exactly. Bug #8338 shows 
a way to produce incoherence using only the GADTs extension. (It does need 4 
modules, though.) I conjecture that incoherence is also possible through 
GeneralizedNewtypeDeriving, both as it existed in GHC 7.6.3 and in 7.8, so it's 
not an issue with Coercible, exactly. It's just that Coercible allows you to 
get incoherence with so much less fuss than before!

Wait! I have an idea!
The way I've been describing GND all along has been an abbreviation. GHC does 
not coerce a dictionary from, say, Ord Int to Ord Age. Instead, GHC mints a 
fresh dictionary for Ord Age where all the methods are implemented as coerced 
versions of the methods for Ord Int. (I'm not sure why it's implemented this 
way, which is why I've elided this detail in just about every conversation on 
the topic.) With this in mind, I have a proposal:

1) All parameters of all classes have nominal role.
2) Classes also store one extra bit per parameter, saying whether all uses of 
that parameter are representational. Essentially, this bit says whether that 
parameter is suitable for GND. (Currently, we could just store for the last 
parameter, but we can imagine extensions to the GND mechanism for other 
parameters.)

Because GND is implemented using coercions on each piece instead of wholesale, 
the nominal roles on classes won't get in the way of proper use of GND. An 
experiment (see below for details) also confirms that even superclasses work 
well with this idea -- the superclasses aren't coerced.

Under this proposal, dictionaries can never be coerced, but GND would still 
seem to work.

Thoughts?

Richard

Experiment:

newtype Age = MkAge Int

instance Eq Age where
  _ == _ = False

deriving instance Ord Age

useOrdInstance :: Ord a => a -> Bool
useOrdInstance x = (x == x)

What does `useOrdInstance (MkAge 5)` yield? It yields `False` (in HEAD). This 
means that the existing GND mechanism (I didn't change anything around this 
part of the code) uses superclass instances for the *newtype*, not for the 
*base type*. So, even with superclasses, class dictionaries don't need to be 
coerced.

Does GND make sense in cases where the superclasses aren't also derived? If I 
had a type T whose Ord instance made use of the Eq instance for some reason, 
and then I made a newtype T' with a new Eq instance and a GND Ord instance, the 
calls to (==) in the Ord instance will refer to the T implementation, right?

That seems like what'd we'd expect GND to do, but is it ever something you 
would want to do?

--
Dave Menendez mailto:d...@zednenem.com>>

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: default roles

[David Menendez]

On Wed, Oct 9, 2013 at 3:21 PM, Richard Eisenberg  wrote:

> Now I think we're on the same page, and I *am* a little worried about the
> sky falling because of this. (That's not a euphemism -- I'm only a little
> worried.)
>
> Well, maybe I should be more worried.
>
> The whole idea of roles is to protect against type-unsoundness. They are
> doing a great job of that here -- no problem that we've discussed in this
> thread is a threat against type safety.
>
> The issue immediately at hand is about coherence (or perhaps you call it
> confluence) of instances. Roles do not address the issue of coherence at
> all, and thus they fail to protect against coherence attacks. It would take
> More Thought to reformulate roles (or devise something else) to handle
> coherence.
>
> It's worth pointing out that this isn't a new problem, exactly. Bug #8338
> shows a way to produce incoherence using only the GADTs extension. (It does
> need 4 modules, though.) I conjecture that incoherence is also possible
> through GeneralizedNewtypeDeriving, both as it existed in GHC 7.6.3 and in
> 7.8, so it's not an issue with Coercible, exactly. It's just that Coercible
> allows you to get incoherence with so much less fuss than before!
>
> Wait! I have an idea!
> The way I've been describing GND all along has been an abbreviation. GHC
> does not coerce a dictionary from, say, Ord Int to Ord Age. Instead, GHC
> mints a fresh dictionary for Ord Age where all the methods are implemented
> as coerced versions of the methods for Ord Int. (I'm not sure why it's
> implemented this way, which is why I've elided this detail in just about
> every conversation on the topic.) With this in mind, I have a proposal:
>
> 1) All parameters of all classes have nominal role.
> 2) Classes also store one extra bit per parameter, saying whether all uses
> of that parameter are representational. Essentially, this bit says whether
> that parameter is suitable for GND. (Currently, we could just store for the
> last parameter, but we can imagine extensions to the GND mechanism for
> other parameters.)
>
> Because GND is implemented using coercions on each piece instead of
> wholesale, the nominal roles on classes won't get in the way of proper use
> of GND. An experiment (see below for details) also confirms that even
> superclasses work well with this idea -- the superclasses aren't coerced.
>
> Under this proposal, dictionaries can never be coerced, but GND would
> still seem to work.
>
> Thoughts?
>
> Richard
>
> Experiment:
>
> newtype Age = MkAge Int
>
> instance Eq Age where
>   _ == _ = False
>
> deriving instance Ord Age
>
> useOrdInstance :: Ord a => a -> Bool
> useOrdInstance x = (x == x)
>
>
> What does `useOrdInstance (MkAge 5)` yield? It yields `False` (in HEAD).
> This means that the existing GND mechanism (I didn't change anything around
> this part of the code) uses superclass instances for the *newtype*, not for
> the *base type*. So, even with superclasses, class dictionaries don't need
> to be coerced.
>

Does GND make sense in cases where the superclasses aren't also derived? If
I had a type T whose Ord instance made use of the Eq instance for some
reason, and then I made a newtype T' with a new Eq instance and a GND Ord
instance, the calls to (==) in the Ord instance will refer to the T
implementation, right?

That seems like what'd we'd expect GND to do, but is it ever something you
would want to do?

-- 
Dave Menendez 

___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Re: default roles

[Joachim Breitner]

Hi,

Am Mittwoch, den 09.10.2013, 23:18 -0400 schrieb Richard Eisenberg:
> On Oct 9, 2013, at 6:24 PM, Joachim Breitner  wrote:
> > 
> > So the conclusion is indeed: Let type class constraints have a nominal
> > role, and all is fine.
> 
> But, then it would seem that any class with a superclass wouldn't be
> compatible with GND. Do you see that detail as a consequence of this
> design?
> 
> I think this approach might work, but I'm not yet convinced.

given that we coerce the fields individually already, and are not going
to change that, I don’t think there is a problem with superclasses.

Even more so: The instance datatype of the subclass will have a field
that contains the instance _datatype_ of the superclass, not a field
with a type class constraint (because as soon as we talk about
dictionaries, we are in Core, where the instance _type functions_ have
already been resolved), which would be representational.

It probably is confusing that (IIRC) the same TyCon is used for both
uses of classes: At the Haskell level, as a function on types; at the
core level, as a regular datatype.

Greetings,
Joachim

-- 
Joachim “nomeata” Breitner
  m...@joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nome...@joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nome...@debian.org


signature.asc
Description: This is a digitally signed message part
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users