Richard Eisenberg | 7 Oct 15:26 2013

default roles

As you may have heard, /roles/ will be introduced with GHC 7.8. Roles are a mechanism to allow for safe 0-cost conversions between newtypes and their base types. GeneralizedNewtypeDeriving (GND) already did this for class instances, but in an unsafe way -- the feature has essentially been retrofitted to work with roles. This means that some uses of GND that appear to be unsafe will no longer work. See the wiki page [1] or slides from a recent presentation [2] for more info.


I am writing because it's unclear what the *default* role should be -- that is, should GND be allowed by default? Examples follow, but the critical issue is this:

* If we allow GND by default anywhere it is type-safe, datatypes (even those that don't export constructors) will not be abstract by default. Library writers would have to use a role annotation everywhere they wish to declare a datatype they do not want users to be able to inspect. (Roles still keep type-*un*safe GND from happening.)

* If we disallow GND by default, then perhaps lots of current uses of GND will break. Library writers will have to explicitly declare when they wish to permit GND involving a datatype.

Which do we think is better?

Examples: The chief example demonstrating the problem is (a hypothetical implementation of) Set:

> module Set (Set) where   -- note: no constructors exported!
>
> data Set a = MkSet [a]
> insert :: Ord a => a -> Set a -> Set a
> ...

> {-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving #-}
> module Client where
>
> import Set
>
> newtype Age = MkAge Int deriving Eq
>
> instance Ord Age where
>   (MkAge a) `compare` (MkAge b) = b `compare` a   -- flip operands, reversing the order
>
> class HasSet a where
>   getSet :: Set a
>
> instance HasSet Int where
>   getSet = insert 2 (insert 5 empty)
>
> deriving instance HasSet Age
>
> good :: Set Int
> good = getSet
>
> bad :: Set Age
> bad = getSet

According to the way GND works, `good` and `bad` will have the same runtime representation. But, using Set operations on `bad` would indeed be bad -- because the Ord instance for Age is different than that for Int, Set operations will fail unexpectedly on `bad`. The problem is that Set should really be abstract, but we've been able to break this abstraction with GND. Note that there is no type error in these operations, just wrong behavior.

So, if we default to *no* GND, then the "deriving" line above would have an error and this problem wouldn't happen. If we default to *allowing* GND, then the writer of Set would have to include
> type role Set nominal
in the definition of the Set module to prevent the use of GND. (Why that peculiar annotation? See the linked further reading, above.)

Although it doesn't figure in this example, a library writer who wishes to allow GND in the default-no scenario would need a similar annotation
> type role Foo representational
to allow it.

There are clearly reasons for and against either decision, but which is better? Let the users decide!

Discussion time: 2 weeks.

Thanks!
Richard
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
migmit | 7 Oct 21:55 2013
Picon

Re: default roles

Something bugs me here.

If some type variable a is used as a parameter to another type variable t, then it's considered nominal. I suppose, that's because it is possible that it would be nominal for some specific t. But we might just know that in our application it's always representational, for every possible t that we would ever use. In this case, we might want to a) explicitly state that t's type parameter should always be representational, and b) at the same time make a representational. Seems like a probable scenario to me.

Отправлено с iPad

07 окт. 2013 г., в 17:26, Richard Eisenberg <eir <at> cis.upenn.edu> написал(а):

As you may have heard, /roles/ will be introduced with GHC 7.8. Roles are a mechanism to allow for safe 0-cost conversions between newtypes and their base types. GeneralizedNewtypeDeriving (GND) already did this for class instances, but in an unsafe way -- the feature has essentially been retrofitted to work with roles. This means that some uses of GND that appear to be unsafe will no longer work. See the wiki page [1] or slides from a recent presentation [2] for more info.


I am writing because it's unclear what the *default* role should be -- that is, should GND be allowed by default? Examples follow, but the critical issue is this:

* If we allow GND by default anywhere it is type-safe, datatypes (even those that don't export constructors) will not be abstract by default. Library writers would have to use a role annotation everywhere they wish to declare a datatype they do not want users to be able to inspect. (Roles still keep type-*un*safe GND from happening.)

* If we disallow GND by default, then perhaps lots of current uses of GND will break. Library writers will have to explicitly declare when they wish to permit GND involving a datatype.

Which do we think is better?

Examples: The chief example demonstrating the problem is (a hypothetical implementation of) Set:

> module Set (Set) where   -- note: no constructors exported!
>
> data Set a = MkSet [a]
> insert :: Ord a => a -> Set a -> Set a
> ...

> {-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving #-}
> module Client where
>
> import Set
>
> newtype Age = MkAge Int deriving Eq
>
> instance Ord Age where
>   (MkAge a) `compare` (MkAge b) = b `compare` a   -- flip operands, reversing the order
>
> class HasSet a where
>   getSet :: Set a
>
> instance HasSet Int where
>   getSet = insert 2 (insert 5 empty)
>
> deriving instance HasSet Age
>
> good :: Set Int
> good = getSet
>
> bad :: Set Age
> bad = getSet

According to the way GND works, `good` and `bad` will have the same runtime representation. But, using Set operations on `bad` would indeed be bad -- because the Ord instance for Age is different than that for Int, Set operations will fail unexpectedly on `bad`. The problem is that Set should really be abstract, but we've been able to break this abstraction with GND. Note that there is no type error in these operations, just wrong behavior.

So, if we default to *no* GND, then the "deriving" line above would have an error and this problem wouldn't happen. If we default to *allowing* GND, then the writer of Set would have to include
> type role Set nominal
in the definition of the Set module to prevent the use of GND. (Why that peculiar annotation? See the linked further reading, above.)

Although it doesn't figure in this example, a library writer who wishes to allow GND in the default-no scenario would need a similar annotation
> type role Foo representational
to allow it.

There are clearly reasons for and against either decision, but which is better? Let the users decide!

Discussion time: 2 weeks.

Thanks!
Richard
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Richard Eisenberg | 7 Oct 22:16 2013

Re: default roles

You raise an excellent point, and yes, your understanding of how roles work in this case is correct.

The problem with your proposal is that it's rather involved to implement and maintain -- essentially, every type and type variable would need to be annotated with both a role and a kind. (These annotations would generally be invisible to users, but quite apparent to implementors.) The current solution is admittedly incomplete in this area, but it requires tracking roles only for parameters to datatypes and classes. We're waiting to see how important this particular issue is in practice before committing to implementing it (a medium-sized project) and maintaining it into perpetuity.

Richard

On Oct 7, 2013, at 3:55 PM, migmit wrote:

Something bugs me here.

If some type variable a is used as a parameter to another type variable t, then it's considered nominal. I suppose, that's because it is possible that it would be nominal for some specific t. But we might just know that in our application it's always representational, for every possible t that we would ever use. In this case, we might want to a) explicitly state that t's type parameter should always be representational, and b) at the same time make a representational. Seems like a probable scenario to me.

Отправлено с iPad

07 окт. 2013 г., в 17:26, Richard Eisenberg <eir <at> cis.upenn.edu> написал(а):

As you may have heard, /roles/ will be introduced with GHC 7.8. Roles are a mechanism to allow for safe 0-cost conversions between newtypes and their base types. GeneralizedNewtypeDeriving (GND) already did this for class instances, but in an unsafe way -- the feature has essentially been retrofitted to work with roles. This means that some uses of GND that appear to be unsafe will no longer work. See the wiki page [1] or slides from a recent presentation [2] for more info.


I am writing because it's unclear what the *default* role should be -- that is, should GND be allowed by default? Examples follow, but the critical issue is this:

* If we allow GND by default anywhere it is type-safe, datatypes (even those that don't export constructors) will not be abstract by default. Library writers would have to use a role annotation everywhere they wish to declare a datatype they do not want users to be able to inspect. (Roles still keep type-*un*safe GND from happening.)

* If we disallow GND by default, then perhaps lots of current uses of GND will break. Library writers will have to explicitly declare when they wish to permit GND involving a datatype.

Which do we think is better?

Examples: The chief example demonstrating the problem is (a hypothetical implementation of) Set:

> module Set (Set) where   -- note: no constructors exported!
>
> data Set a = MkSet [a]
> insert :: Ord a => a -> Set a -> Set a
> ...

> {-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving #-}
> module Client where
>
> import Set
>
> newtype Age = MkAge Int deriving Eq
>
> instance Ord Age where
>   (MkAge a) `compare` (MkAge b) = b `compare` a   -- flip operands, reversing the order
>
> class HasSet a where
>   getSet :: Set a
>
> instance HasSet Int where
>   getSet = insert 2 (insert 5 empty)
>
> deriving instance HasSet Age
>
> good :: Set Int
> good = getSet
>
> bad :: Set Age
> bad = getSet

According to the way GND works, `good` and `bad` will have the same runtime representation. But, using Set operations on `bad` would indeed be bad -- because the Ord instance for Age is different than that for Int, Set operations will fail unexpectedly on `bad`. The problem is that Set should really be abstract, but we've been able to break this abstraction with GND. Note that there is no type error in these operations, just wrong behavior.

So, if we default to *no* GND, then the "deriving" line above would have an error and this problem wouldn't happen. If we default to *allowing* GND, then the writer of Set would have to include
> type role Set nominal
in the definition of the Set module to prevent the use of GND. (Why that peculiar annotation? See the linked further reading, above.)

Although it doesn't figure in this example, a library writer who wishes to allow GND in the default-no scenario would need a similar annotation
> type role Foo representational
to allow it.

There are clearly reasons for and against either decision, but which is better? Let the users decide!

Discussion time: 2 weeks.

Thanks!
Richard
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
migmit | 7 Oct 23:16 2013
Picon

Re: default roles

Well, it seems to be exactly like type classes. What if instead of implementing this "roles" we simply add a type class, say, "HasRepresentationalArgument", which can be (and is) derived automatically. Of course, multiple arguments could be a problem, but, since we already have polymorphic kinds, not a big one.

Отправлено с iPad

08 окт. 2013 г., в 0:16, Richard Eisenberg <eir <at> cis.upenn.edu> написал(а):

You raise an excellent point, and yes, your understanding of how roles work in this case is correct.

The problem with your proposal is that it's rather involved to implement and maintain -- essentially, every type and type variable would need to be annotated with both a role and a kind. (These annotations would generally be invisible to users, but quite apparent to implementors.) The current solution is admittedly incomplete in this area, but it requires tracking roles only for parameters to datatypes and classes. We're waiting to see how important this particular issue is in practice before committing to implementing it (a medium-sized project) and maintaining it into perpetuity.

Richard

On Oct 7, 2013, at 3:55 PM, migmit wrote:

Something bugs me here.

If some type variable a is used as a parameter to another type variable t, then it's considered nominal. I suppose, that's because it is possible that it would be nominal for some specific t. But we might just know that in our application it's always representational, for every possible t that we would ever use. In this case, we might want to a) explicitly state that t's type parameter should always be representational, and b) at the same time make a representational. Seems like a probable scenario to me.

Отправлено с iPad

07 окт. 2013 г., в 17:26, Richard Eisenberg <eir <at> cis.upenn.edu> написал(а):

As you may have heard, /roles/ will be introduced with GHC 7.8. Roles are a mechanism to allow for safe 0-cost conversions between newtypes and their base types. GeneralizedNewtypeDeriving (GND) already did this for class instances, but in an unsafe way -- the feature has essentially been retrofitted to work with roles. This means that some uses of GND that appear to be unsafe will no longer work. See the wiki page [1] or slides from a recent presentation [2] for more info.


I am writing because it's unclear what the *default* role should be -- that is, should GND be allowed by default? Examples follow, but the critical issue is this:

* If we allow GND by default anywhere it is type-safe, datatypes (even those that don't export constructors) will not be abstract by default. Library writers would have to use a role annotation everywhere they wish to declare a datatype they do not want users to be able to inspect. (Roles still keep type-*un*safe GND from happening.)

* If we disallow GND by default, then perhaps lots of current uses of GND will break. Library writers will have to explicitly declare when they wish to permit GND involving a datatype.

Which do we think is better?

Examples: The chief example demonstrating the problem is (a hypothetical implementation of) Set:

> module Set (Set) where   -- note: no constructors exported!
>
> data Set a = MkSet [a]
> insert :: Ord a => a -> Set a -> Set a
> ...

> {-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving #-}
> module Client where
>
> import Set
>
> newtype Age = MkAge Int deriving Eq
>
> instance Ord Age where
>   (MkAge a) `compare` (MkAge b) = b `compare` a   -- flip operands, reversing the order
>
> class HasSet a where
>   getSet :: Set a
>
> instance HasSet Int where
>   getSet = insert 2 (insert 5 empty)
>
> deriving instance HasSet Age
>
> good :: Set Int
> good = getSet
>
> bad :: Set Age
> bad = getSet

According to the way GND works, `good` and `bad` will have the same runtime representation. But, using Set operations on `bad` would indeed be bad -- because the Ord instance for Age is different than that for Int, Set operations will fail unexpectedly on `bad`. The problem is that Set should really be abstract, but we've been able to break this abstraction with GND. Note that there is no type error in these operations, just wrong behavior.

So, if we default to *no* GND, then the "deriving" line above would have an error and this problem wouldn't happen. If we default to *allowing* GND, then the writer of Set would have to include
> type role Set nominal
in the definition of the Set module to prevent the use of GND. (Why that peculiar annotation? See the linked further reading, above.)

Although it doesn't figure in this example, a library writer who wishes to allow GND in the default-no scenario would need a similar annotation
> type role Foo representational
to allow it.

There are clearly reasons for and against either decision, but which is better? Let the users decide!

Discussion time: 2 weeks.

Thanks!
Richard
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Ganesh Sittampalam | 7 Oct 22:33 2013
Picon

Re: default roles

Is it possible to tie the role to whether the data constructor is
visible or not?

On 07/10/2013 14:26, Richard Eisenberg wrote:
> As you may have heard, /roles/ will be introduced with GHC 7.8. Roles
> are a mechanism to allow for safe 0-cost conversions between newtypes
> and their base types. GeneralizedNewtypeDeriving (GND) already did this
> for class instances, but in an unsafe way -- the feature has essentially
> been retrofitted to work with roles. This means that some uses of GND
> that appear to be unsafe will no longer work. See the wiki page [1] or
> slides from a recent presentation [2] for more info.
> 
> [1] : http://ghc.haskell.org/trac/ghc/wiki/Roles
> [2] : http://www.cis.upenn.edu/~eir/papers/2013/roles/roles-slides.pdf
> 
> I am writing because it's unclear what the *default* role should be --
> that is, should GND be allowed by default? Examples follow, but the
> critical issue is this:
> 
> * If we allow GND by default anywhere it is type-safe, datatypes (even
> those that don't export constructors) will not be abstract by default.
> Library writers would have to use a role annotation everywhere they wish
> to declare a datatype they do not want users to be able to inspect.
> (Roles still keep type-*un*safe GND from happening.)
> 
> * If we disallow GND by default, then perhaps lots of current uses of
> GND will break. Library writers will have to explicitly declare when
> they wish to permit GND involving a datatype.
> 
> Which do we think is better?
> 
> Examples: The chief example demonstrating the problem is (a hypothetical
> implementation of) Set:
> 
>> module Set (Set) where   -- note: no constructors exported!
>>
>> data Set a = MkSet [a]
>> insert :: Ord a => a -> Set a -> Set a
>> ...
> 
>> {-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving #-}
>> module Client where
>>
>> import Set
>>
>> newtype Age = MkAge Int deriving Eq
>>
>> instance Ord Age where
>>   (MkAge a) `compare` (MkAge b) = b `compare` a   -- flip operands,
> reversing the order
>>
>> class HasSet a where
>>   getSet :: Set a
>>
>> instance HasSet Int where
>>   getSet = insert 2 (insert 5 empty)
>>
>> deriving instance HasSet Age
>>
>> good :: Set Int
>> good = getSet
>>
>> bad :: Set Age
>> bad = getSet
> 
> According to the way GND works, `good` and `bad` will have the same
> runtime representation. But, using Set operations on `bad` would indeed
> be bad -- because the Ord instance for Age is different than that for
> Int, Set operations will fail unexpectedly on `bad`. The problem is that
> Set should really be abstract, but we've been able to break this
> abstraction with GND. Note that there is no type error in these
> operations, just wrong behavior.
> 
> So, if we default to *no* GND, then the "deriving" line above would have
> an error and this problem wouldn't happen. If we default to *allowing*
> GND, then the writer of Set would have to include
>> type role Set nominal
> in the definition of the Set module to prevent the use of GND. (Why that
> peculiar annotation? See the linked further reading, above.)
> 
> Although it doesn't figure in this example, a library writer who wishes
> to allow GND in the default-no scenario would need a similar annotation
>> type role Foo representational
> to allow it.
> 
> There are clearly reasons for and against either decision, but which is
> better? Let the users decide!
> 
> Discussion time: 2 weeks.
> 
> Thanks!
> Richard
> 
> 
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users <at> haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> 
Richard Eisenberg | 8 Oct 04:21 2013

Re: default roles

We considered this for a while, but it led to a strange design -- to do it right, you would have to import all
constructors for all datatypes *recursively* out to the leaves, starting at the datatypes mentioned in
the class for which you wanted to use GND. This would mean potentially a whole lot of imports for symbols not
actually used in the text of a program.

Richard

On Oct 7, 2013, at 4:33 PM, Ganesh Sittampalam <ganesh <at> earth.li> wrote:

> Is it possible to tie the role to whether the data constructor is
> visible or not?
> 
> On 07/10/2013 14:26, Richard Eisenberg wrote:
>> As you may have heard, /roles/ will be introduced with GHC 7.8. Roles
>> are a mechanism to allow for safe 0-cost conversions between newtypes
>> and their base types. GeneralizedNewtypeDeriving (GND) already did this
>> for class instances, but in an unsafe way -- the feature has essentially
>> been retrofitted to work with roles. This means that some uses of GND
>> that appear to be unsafe will no longer work. See the wiki page [1] or
>> slides from a recent presentation [2] for more info.
>> 
>> [1] : http://ghc.haskell.org/trac/ghc/wiki/Roles
>> [2] : http://www.cis.upenn.edu/~eir/papers/2013/roles/roles-slides.pdf
>> 
>> I am writing because it's unclear what the *default* role should be --
>> that is, should GND be allowed by default? Examples follow, but the
>> critical issue is this:
>> 
>> * If we allow GND by default anywhere it is type-safe, datatypes (even
>> those that don't export constructors) will not be abstract by default.
>> Library writers would have to use a role annotation everywhere they wish
>> to declare a datatype they do not want users to be able to inspect.
>> (Roles still keep type-*un*safe GND from happening.)
>> 
>> * If we disallow GND by default, then perhaps lots of current uses of
>> GND will break. Library writers will have to explicitly declare when
>> they wish to permit GND involving a datatype.
>> 
>> Which do we think is better?
>> 
>> Examples: The chief example demonstrating the problem is (a hypothetical
>> implementation of) Set:
>> 
>>> module Set (Set) where   -- note: no constructors exported!
>>> 
>>> data Set a = MkSet [a]
>>> insert :: Ord a => a -> Set a -> Set a
>>> ...
>> 
>>> {-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving #-}
>>> module Client where
>>> 
>>> import Set
>>> 
>>> newtype Age = MkAge Int deriving Eq
>>> 
>>> instance Ord Age where
>>>  (MkAge a) `compare` (MkAge b) = b `compare` a   -- flip operands,
>> reversing the order
>>> 
>>> class HasSet a where
>>>  getSet :: Set a
>>> 
>>> instance HasSet Int where
>>>  getSet = insert 2 (insert 5 empty)
>>> 
>>> deriving instance HasSet Age
>>> 
>>> good :: Set Int
>>> good = getSet
>>> 
>>> bad :: Set Age
>>> bad = getSet
>> 
>> According to the way GND works, `good` and `bad` will have the same
>> runtime representation. But, using Set operations on `bad` would indeed
>> be bad -- because the Ord instance for Age is different than that for
>> Int, Set operations will fail unexpectedly on `bad`. The problem is that
>> Set should really be abstract, but we've been able to break this
>> abstraction with GND. Note that there is no type error in these
>> operations, just wrong behavior.
>> 
>> So, if we default to *no* GND, then the "deriving" line above would have
>> an error and this problem wouldn't happen. If we default to *allowing*
>> GND, then the writer of Set would have to include
>>> type role Set nominal
>> in the definition of the Set module to prevent the use of GND. (Why that
>> peculiar annotation? See the linked further reading, above.)
>> 
>> Although it doesn't figure in this example, a library writer who wishes
>> to allow GND in the default-no scenario would need a similar annotation
>>> type role Foo representational
>> to allow it.
>> 
>> There are clearly reasons for and against either decision, but which is
>> better? Let the users decide!
>> 
>> Discussion time: 2 weeks.
>> 
>> Thanks!
>> Richard
>> 
>> 
>> _______________________________________________
>> Glasgow-haskell-users mailing list
>> Glasgow-haskell-users <at> haskell.org
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>> 
> 
José Pedro Magalhães | 8 Oct 10:01 2013
Picon

Re: default roles

Hi,

On Tue, Oct 8, 2013 at 3:21 AM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
We considered this for a while, but it led to a strange design -- to do it right, you would have to import all constructors for all datatypes *recursively* out to the leaves, starting at the datatypes mentioned in the class for which you wanted to use GND. This would mean potentially a whole lot of imports for symbols not actually used in the text of a program.

I'm not sure I understand why constructors are involved in this. Wouldn't something like
the following potentially be useful?

data Role = Nominal | Representational | Phantom | Fun Role Role

type family HasRole (t :: k) :: Role

data MyData a b = MyData a
data MyGADT a b where MyGADT :: MyGADT a Int

type instance HasRole MyData      = Fun Representational Phantom
type instance HasRole MyGADT      = Fun Representational Nominal
type instance HasRole Traversable = Nominal


HasRole instances would be automatically given by GHC.


Cheers,
Pedro


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Richard Eisenberg | 8 Oct 15:23 2013

Re: default roles

Pedro is suggesting a way for a Haskell type-level program to gain access to role information. This might indeed be useful, but it doesn't seem terribly related to the problem of defaults / abstraction. The problem has to do with definitions like these:

> module A where
> data S a b = S1 a | S2 b
> data T a b = MkT (S a b)

> module B where
> import A ( {- what goes here? -} )
>
> class C a where
>   mkT :: T Bool a
>
> instance C Int where ...
> newtype Age = MkAge Int deriving C

What constructors do we need in order to convert the (C Int) instance to (C Age) by hand? To me, it looks like we need MkT and S2, but not S1. Yet, this is not obvious and seems to be quite confusing.

I hope this helps understanding the issue!
Richard

On Oct 8, 2013, at 4:01 AM, José Pedro Magalhães <dreixel <at> gmail.com> wrote:

Hi,

On Tue, Oct 8, 2013 at 3:21 AM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
We considered this for a while, but it led to a strange design -- to do it right, you would have to import all constructors for all datatypes *recursively* out to the leaves, starting at the datatypes mentioned in the class for which you wanted to use GND. This would mean potentially a whole lot of imports for symbols not actually used in the text of a program.

I'm not sure I understand why constructors are involved in this. Wouldn't something like
the following potentially be useful?

data Role = Nominal | Representational | Phantom | Fun Role Role

type family HasRole (t :: k) :: Role

data MyData a b = MyData a
data MyGADT a b where MyGADT :: MyGADT a Int

type instance HasRole MyData      = Fun Representational Phantom
type instance HasRole MyGADT      = Fun Representational Nominal
type instance HasRole Traversable = Nominal


HasRole instances would be automatically given by GHC.


Cheers,
Pedro



_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Ganesh Sittampalam | 9 Oct 14:45 2013
Picon

Re: default roles

I think it would be ok to expect the constructors to be visible, even though it might need to a lot being needed.

BTW I think you might need S1 visible as well otherwise how would you convert (S1 True :: S Bool Int) into (S1 True :: S Bool Age)?

If you don't derive the role from constructor visibility then I think it should fail-safe and default to the nominal role - valid Haskell 2010 code shouldn't be exposed to an abstraction leak just because it's GHC compiling it.


On 08/10/2013 14:23, Richard Eisenberg wrote:
Pedro is suggesting a way for a Haskell type-level program to gain access to role information. This might indeed be useful, but it doesn't seem terribly related to the problem of defaults / abstraction. The problem has to do with definitions like these:

> module A where
> data S a b = S1 a | S2 b
> data T a b = MkT (S a b)

> module B where
> import A ( {- what goes here? -} )
>
> class C a where
>   mkT :: T Bool a
>
> instance C Int where ...
> newtype Age = MkAge Int deriving C

What constructors do we need in order to convert the (C Int) instance to (C Age) by hand? To me, it looks like we need MkT and S2, but not S1. Yet, this is not obvious and seems to be quite confusing.

I hope this helps understanding the issue!
Richard

On Oct 8, 2013, at 4:01 AM, José Pedro Magalhães <dreixel <at> gmail.com> wrote:

Hi,

On Tue, Oct 8, 2013 at 3:21 AM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
We considered this for a while, but it led to a strange design -- to do it right, you would have to import all constructors for all datatypes *recursively* out to the leaves, starting at the datatypes mentioned in the class for which you wanted to use GND. This would mean potentially a whole lot of imports for symbols not actually used in the text of a program.

I'm not sure I understand why constructors are involved in this. Wouldn't something like
the following potentially be useful?

data Role = Nominal | Representational | Phantom | Fun Role Role

type family HasRole (t :: k) :: Role

data MyData a b = MyData a
data MyGADT a b where MyGADT :: MyGADT a Int

type instance HasRole MyData      = Fun Representational Phantom
type instance HasRole MyGADT      = Fun Representational Nominal
type instance HasRole Traversable = Nominal


HasRole instances would be automatically given by GHC.


Cheers,
Pedro




_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Miguel | 8 Oct 16:49 2013
Picon

Re: default roles

I don't understand it either.

Type family solution, however, seems wrong. See, if we, somehow, make something nominal when it has to be representational — well, some code won't compile, but nothing really bad happens. If, on the other hand, we by some miracle make something representational when in should be nominal — we can get a runtime error. It seems to be very similar to how type classes work, with "nominal" being the default, and "representational" a type class.

Consider, for example, the "Tricky" example from the slides, slightly changed:

data Tricky2 a b c = MkTricky2 (a c) (b c)

Currently parameter c would be nominal. I suggest that it should be representational if and only if it's representational for BOTH a and b. WIth type classes it would be very simple:

instance (HasRepresentationalParameter a, HasRepresentationalParameter b) => HasRepresentationalParameter (Tricky2 a b)

With type families... well, apparently I don't have enough milliolegs to figure out how to do it.


On Tue, Oct 8, 2013 at 12:01 PM, José Pedro Magalhães <dreixel <at> gmail.com> wrote:
Hi,

On Tue, Oct 8, 2013 at 3:21 AM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
We considered this for a while, but it led to a strange design -- to do it right, you would have to import all constructors for all datatypes *recursively* out to the leaves, starting at the datatypes mentioned in the class for which you wanted to use GND. This would mean potentially a whole lot of imports for symbols not actually used in the text of a program.

I'm not sure I understand why constructors are involved in this. Wouldn't something like
the following potentially be useful?

data Role = Nominal | Representational | Phantom | Fun Role Role

type family HasRole (t :: k) :: Role

data MyData a b = MyData a
data MyGADT a b where MyGADT :: MyGADT a Int

type instance HasRole MyData      = Fun Representational Phantom
type instance HasRole MyGADT      = Fun Representational Nominal
type instance HasRole Traversable = Nominal


HasRole instances would be automatically given by GHC.


Cheers,
Pedro



_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Richard Eisenberg | 8 Oct 17:02 2013

Re: default roles

Perhaps I can spot the source of the confusion: there seem to be 2 different conversations going on here!

1: How to fit roles in with the ability to declare a datatype to be abstract. Should a library author be required to use a role annotation to make an abstract datatype, or should a library author be required to use a role annotation to allow GND with a datatype?

2: Some form of role abstraction, where an argument to a type parameter might get a representational role, depending on the role of some other variable. Using typeclasses is the current proposal for how to do this, and it in migmit's email below. Pedro also suggests a type families approach.


My initial email was seeking advice on issue #1.

As for #2: Using typeclasses here might be a decent surface syntax for the feature of role abstraction, but the automatic generation of instances, etc., would seem to require deep and pervasive magic under the hood. Essentially, every type and type variable would need to be annotated with both a kind and a role, significantly complicating GHC's type system. The question would be whether or not this upfront and ongoing investment is worth it.

Thanks,
Richard

On Oct 8, 2013, at 10:49 AM, Miguel <migmit <at> gmail.com> wrote:

I don't understand it either.

Type family solution, however, seems wrong. See, if we, somehow, make something nominal when it has to be representational — well, some code won't compile, but nothing really bad happens. If, on the other hand, we by some miracle make something representational when in should be nominal — we can get a runtime error. It seems to be very similar to how type classes work, with "nominal" being the default, and "representational" a type class.

Consider, for example, the "Tricky" example from the slides, slightly changed:

data Tricky2 a b c = MkTricky2 (a c) (b c)

Currently parameter c would be nominal. I suggest that it should be representational if and only if it's representational for BOTH a and b. WIth type classes it would be very simple:

instance (HasRepresentationalParameter a, HasRepresentationalParameter b) => HasRepresentationalParameter (Tricky2 a b)

With type families... well, apparently I don't have enough milliolegs to figure out how to do it.


On Tue, Oct 8, 2013 at 12:01 PM, José Pedro Magalhães <dreixel <at> gmail.com> wrote:
Hi,

On Tue, Oct 8, 2013 at 3:21 AM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
We considered this for a while, but it led to a strange design -- to do it right, you would have to import all constructors for all datatypes *recursively* out to the leaves, starting at the datatypes mentioned in the class for which you wanted to use GND. This would mean potentially a whole lot of imports for symbols not actually used in the text of a program.

I'm not sure I understand why constructors are involved in this. Wouldn't something like
the following potentially be useful?

data Role = Nominal | Representational | Phantom | Fun Role Role

type family HasRole (t :: k) :: Role

data MyData a b = MyData a
data MyGADT a b where MyGADT :: MyGADT a Int

type instance HasRole MyData      = Fun Representational Phantom
type instance HasRole MyGADT      = Fun Representational Nominal
type instance HasRole Traversable = Nominal


HasRole instances would be automatically given by GHC.


Cheers,
Pedro



_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users



_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Iavor Diatchki | 9 Oct 18:07 2013
Picon

Re: default roles

Hello,

My preference would be for the following design:

1. The default datatypes for roles are Nominal, but programmers can add annotations to relax this.
2. Generlized newtype deriving works as follows:  we can coerce a dictionary for `C R` into `C T`, as long as we can coerce the types of all methods instantiated with `R`, into the corresponding types instantiated with `T`.  In other words, we are pretending that we are implementing all methods by using `coerce`.

As far as I can see this safe, and matches what I'd expect as a programmer.  It also solves the problem with the `Set` example: because `Set` has a nominal parameter, we cannot coerce `Set Int` into `Set MyAge` and, hence, we cannot derive an instance of `MyAge` for `HasSet`.  An added benefit of this approach is that when newtype deriving fails, we can give a nicer error saying exactly which method causes the problem.

-Iavor






On Mon, Oct 7, 2013 at 6:26 AM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
As you may have heard, /roles/ will be introduced with GHC 7.8. Roles are a mechanism to allow for safe 0-cost conversions between newtypes and their base types. GeneralizedNewtypeDeriving (GND) already did this for class instances, but in an unsafe way -- the feature has essentially been retrofitted to work with roles. This means that some uses of GND that appear to be unsafe will no longer work. See the wiki page [1] or slides from a recent presentation [2] for more info.


I am writing because it's unclear what the *default* role should be -- that is, should GND be allowed by default? Examples follow, but the critical issue is this:

* If we allow GND by default anywhere it is type-safe, datatypes (even those that don't export constructors) will not be abstract by default. Library writers would have to use a role annotation everywhere they wish to declare a datatype they do not want users to be able to inspect. (Roles still keep type-*un*safe GND from happening.)

* If we disallow GND by default, then perhaps lots of current uses of GND will break. Library writers will have to explicitly declare when they wish to permit GND involving a datatype.

Which do we think is better?

Examples: The chief example demonstrating the problem is (a hypothetical implementation of) Set:

> module Set (Set) where   -- note: no constructors exported!
>
> data Set a = MkSet [a]
> insert :: Ord a => a -> Set a -> Set a
> ...

> {-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving #-}
> module Client where
>
> import Set
>
> newtype Age = MkAge Int deriving Eq
>
> instance Ord Age where
>   (MkAge a) `compare` (MkAge b) = b `compare` a   -- flip operands, reversing the order
>
> class HasSet a where
>   getSet :: Set a
>
> instance HasSet Int where
>   getSet = insert 2 (insert 5 empty)
>
> deriving instance HasSet Age
>
> good :: Set Int
> good = getSet
>
> bad :: Set Age
> bad = getSet

According to the way GND works, `good` and `bad` will have the same runtime representation. But, using Set operations on `bad` would indeed be bad -- because the Ord instance for Age is different than that for Int, Set operations will fail unexpectedly on `bad`. The problem is that Set should really be abstract, but we've been able to break this abstraction with GND. Note that there is no type error in these operations, just wrong behavior.

So, if we default to *no* GND, then the "deriving" line above would have an error and this problem wouldn't happen. If we default to *allowing* GND, then the writer of Set would have to include
> type role Set nominal
in the definition of the Set module to prevent the use of GND. (Why that peculiar annotation? See the linked further reading, above.)

Although it doesn't figure in this example, a library writer who wishes to allow GND in the default-no scenario would need a similar annotation
> type role Foo representational
to allow it.

There are clearly reasons for and against either decision, but which is better? Let the users decide!

Discussion time: 2 weeks.

Thanks!
Richard

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Edward Kmett | 9 Oct 19:55 2013
Picon

Re: default roles

I just noticed there is a pretty big issue with the current default role where typeclasses are concerned!

When implementing Data.Type.Coercion I had to use the fact that I could apply coerce to the arguments of

data Coercion a b where
  Coercion :: Coercible a b => Coercion a b

This makes sense as Coercion itself has two representational arguments.

This struck me as quite clever, so I went to test it further.

data Foo a where 
   Foo :: Eq a => Foo a

newtype Bar = Bar Int
instance Eq Bar where
  _ == _ = False

I fully expected the following to fail:

coerce (Foo :: Foo Int) :: Foo Bar

but instead it succeeded. 

This means I was able to convert a dictionary Eq Int into a dictionary for Eq Bar!

This indicates that Eq (actually all) of the typeclasses are currently marked as having representational, when actually it strikes me that (almost?) none of them should be.

Coercible is the only case I can think of in base of a class with two representational arguments, but this is only valid because we prevent users from defining Coercible instances manually.

If I try again with a new typeclass that has an explicit nominal role

type role Eq nominal
class Eq a
instance Eq Int
instance Eq Bar

then I get the failure to derive Coercible (Foo Int) (Foo Bar) that I'd expect.

This indicates two big issues to me: 

1.) At the very least the default role for type classes should be nominal for each argument. The very point of an instance is to make a nominal distinction after all. =)

2.) It also indicates that making any typeclass with a representational (/ phantom?) argument shouldn't be possible in valid SafeHaskell, as you can use it to subvert the current restrictions on OverlappingInstances.

-Edward


On Wed, Oct 9, 2013 at 12:07 PM, Iavor Diatchki <iavor.diatchki <at> gmail.com> wrote:
Hello,

My preference would be for the following design:

1. The default datatypes for roles are Nominal, but programmers can add annotations to relax this.
2. Generlized newtype deriving works as follows:  we can coerce a dictionary for `C R` into `C T`, as long as we can coerce the types of all methods instantiated with `R`, into the corresponding types instantiated with `T`.  In other words, we are pretending that we are implementing all methods by using `coerce`.

As far as I can see this safe, and matches what I'd expect as a programmer.  It also solves the problem with the `Set` example: because `Set` has a nominal parameter, we cannot coerce `Set Int` into `Set MyAge` and, hence, we cannot derive an instance of `MyAge` for `HasSet`.  An added benefit of this approach is that when newtype deriving fails, we can give a nicer error saying exactly which method causes the problem.

-Iavor






On Mon, Oct 7, 2013 at 6:26 AM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
As you may have heard, /roles/ will be introduced with GHC 7.8. Roles are a mechanism to allow for safe 0-cost conversions between newtypes and their base types. GeneralizedNewtypeDeriving (GND) already did this for class instances, but in an unsafe way -- the feature has essentially been retrofitted to work with roles. This means that some uses of GND that appear to be unsafe will no longer work. See the wiki page [1] or slides from a recent presentation [2] for more info.


I am writing because it's unclear what the *default* role should be -- that is, should GND be allowed by default? Examples follow, but the critical issue is this:

* If we allow GND by default anywhere it is type-safe, datatypes (even those that don't export constructors) will not be abstract by default. Library writers would have to use a role annotation everywhere they wish to declare a datatype they do not want users to be able to inspect. (Roles still keep type-*un*safe GND from happening.)

* If we disallow GND by default, then perhaps lots of current uses of GND will break. Library writers will have to explicitly declare when they wish to permit GND involving a datatype.

Which do we think is better?

Examples: The chief example demonstrating the problem is (a hypothetical implementation of) Set:

> module Set (Set) where   -- note: no constructors exported!
>
> data Set a = MkSet [a]
> insert :: Ord a => a -> Set a -> Set a
> ...

> {-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving #-}
> module Client where
>
> import Set
>
> newtype Age = MkAge Int deriving Eq
>
> instance Ord Age where
>   (MkAge a) `compare` (MkAge b) = b `compare` a   -- flip operands, reversing the order
>
> class HasSet a where
>   getSet :: Set a
>
> instance HasSet Int where
>   getSet = insert 2 (insert 5 empty)
>
> deriving instance HasSet Age
>
> good :: Set Int
> good = getSet
>
> bad :: Set Age
> bad = getSet

According to the way GND works, `good` and `bad` will have the same runtime representation. But, using Set operations on `bad` would indeed be bad -- because the Ord instance for Age is different than that for Int, Set operations will fail unexpectedly on `bad`. The problem is that Set should really be abstract, but we've been able to break this abstraction with GND. Note that there is no type error in these operations, just wrong behavior.

So, if we default to *no* GND, then the "deriving" line above would have an error and this problem wouldn't happen. If we default to *allowing* GND, then the writer of Set would have to include
> type role Set nominal
in the definition of the Set module to prevent the use of GND. (Why that peculiar annotation? See the linked further reading, above.)

Although it doesn't figure in this example, a library writer who wishes to allow GND in the default-no scenario would need a similar annotation
> type role Foo representational
to allow it.

There are clearly reasons for and against either decision, but which is better? Let the users decide!

Discussion time: 2 weeks.

Thanks!
Richard

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users



_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Richard Eisenberg | 9 Oct 20:09 2013

Re: default roles

I don't quite agree with your analysis, Edward.

Eq can be auto-derived, so it makes for a confusing example. Let's replace Eq in your example with this class:

> class C a where
>  c_meth :: a -> a -> Bool

Then, your example leads to the same embarrassing state of affairs: coercing a dictionary for (C Int) to one for (C Bar).

But, I would argue that we still want C's parameter to have a representational role. Why? Consider this:

> data Blargh = ...
> instance C Blargh where ...
>
> newtype Baz = MkBaz Blargh deriving C

We want that last line to work, using GeneralizedNewtypeDeriving. This hinges on C's parameter's role being representational.

I think that what you've witnessed is a case of bug #8338 (http://ghc.haskell.org/trac/ghc/ticket/8338). This is a problem, in my view, and it seems to touch on roles, but I'm not completely sure of their relationship.

So, I think that classes should keep their representational roles (regardless of the decision on datatypes -- Haskell doesn't really support "abstract" classes), but perhaps we have to find a way to stop these incoherent instances from forming. Maybe the use of a constraint makes a datatype's role be nominal?

Richard

On Oct 9, 2013, at 1:55 PM, Edward Kmett <ekmett <at> gmail.com> wrote:

I just noticed there is a pretty big issue with the current default role where typeclasses are concerned!

When implementing Data.Type.Coercion I had to use the fact that I could apply coerce to the arguments of

data Coercion a b where
  Coercion :: Coercible a b => Coercion a b

This makes sense as Coercion itself has two representational arguments.

This struck me as quite clever, so I went to test it further.

data Foo a where 
   Foo :: Eq a => Foo a

newtype Bar = Bar Int
instance Eq Bar where
  _ == _ = False

I fully expected the following to fail:

coerce (Foo :: Foo Int) :: Foo Bar

but instead it succeeded. 

This means I was able to convert a dictionary Eq Int into a dictionary for Eq Bar!

This indicates that Eq (actually all) of the typeclasses are currently marked as having representational, when actually it strikes me that (almost?) none of them should be.

Coercible is the only case I can think of in base of a class with two representational arguments, but this is only valid because we prevent users from defining Coercible instances manually.

If I try again with a new typeclass that has an explicit nominal role

type role Eq nominal
class Eq a
instance Eq Int
instance Eq Bar

then I get the failure to derive Coercible (Foo Int) (Foo Bar) that I'd expect.

This indicates two big issues to me: 

1.) At the very least the default role for type classes should be nominal for each argument. The very point of an instance is to make a nominal distinction after all. =)

2.) It also indicates that making any typeclass with a representational (/ phantom?) argument shouldn't be possible in valid SafeHaskell, as you can use it to subvert the current restrictions on OverlappingInstances.

-Edward


On Wed, Oct 9, 2013 at 12:07 PM, Iavor Diatchki <iavor.diatchki <at> gmail.com> wrote:
Hello,

My preference would be for the following design:

1. The default datatypes for roles are Nominal, but programmers can add annotations to relax this.
2. Generlized newtype deriving works as follows:  we can coerce a dictionary for `C R` into `C T`, as long as we can coerce the types of all methods instantiated with `R`, into the corresponding types instantiated with `T`.  In other words, we are pretending that we are implementing all methods by using `coerce`.

As far as I can see this safe, and matches what I'd expect as a programmer.  It also solves the problem with the `Set` example: because `Set` has a nominal parameter, we cannot coerce `Set Int` into `Set MyAge` and, hence, we cannot derive an instance of `MyAge` for `HasSet`.  An added benefit of this approach is that when newtype deriving fails, we can give a nicer error saying exactly which method causes the problem.

-Iavor






On Mon, Oct 7, 2013 at 6:26 AM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
As you may have heard, /roles/ will be introduced with GHC 7.8. Roles are a mechanism to allow for safe 0-cost conversions between newtypes and their base types. GeneralizedNewtypeDeriving (GND) already did this for class instances, but in an unsafe way -- the feature has essentially been retrofitted to work with roles. This means that some uses of GND that appear to be unsafe will no longer work. See the wiki page [1] or slides from a recent presentation [2] for more info.


I am writing because it's unclear what the *default* role should be -- that is, should GND be allowed by default? Examples follow, but the critical issue is this:

* If we allow GND by default anywhere it is type-safe, datatypes (even those that don't export constructors) will not be abstract by default. Library writers would have to use a role annotation everywhere they wish to declare a datatype they do not want users to be able to inspect. (Roles still keep type-*un*safe GND from happening.)

* If we disallow GND by default, then perhaps lots of current uses of GND will break. Library writers will have to explicitly declare when they wish to permit GND involving a datatype.

Which do we think is better?

Examples: The chief example demonstrating the problem is (a hypothetical implementation of) Set:

> module Set (Set) where   -- note: no constructors exported!
>
> data Set a = MkSet [a]
> insert :: Ord a => a -> Set a -> Set a
> ...

> {-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving #-}
> module Client where
>
> import Set
>
> newtype Age = MkAge Int deriving Eq
>
> instance Ord Age where
>   (MkAge a) `compare` (MkAge b) = b `compare` a   -- flip operands, reversing the order
>
> class HasSet a where
>   getSet :: Set a
>
> instance HasSet Int where
>   getSet = insert 2 (insert 5 empty)
>
> deriving instance HasSet Age
>
> good :: Set Int
> good = getSet
>
> bad :: Set Age
> bad = getSet

According to the way GND works, `good` and `bad` will have the same runtime representation. But, using Set operations on `bad` would indeed be bad -- because the Ord instance for Age is different than that for Int, Set operations will fail unexpectedly on `bad`. The problem is that Set should really be abstract, but we've been able to break this abstraction with GND. Note that there is no type error in these operations, just wrong behavior.

So, if we default to *no* GND, then the "deriving" line above would have an error and this problem wouldn't happen. If we default to *allowing* GND, then the writer of Set would have to include
> type role Set nominal
in the definition of the Set module to prevent the use of GND. (Why that peculiar annotation? See the linked further reading, above.)

Although it doesn't figure in this example, a library writer who wishes to allow GND in the default-no scenario would need a similar annotation
> type role Foo representational
to allow it.

There are clearly reasons for and against either decision, but which is better? Let the users decide!

Discussion time: 2 weeks.

Thanks!
Richard

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users



_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users



_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Edward Kmett | 9 Oct 20:52 2013
Picon

Re: default roles

I'd be happy to be wrong. =)

We do seem to have stumbled into a design paradox though.

To make it so you can use roles in GeneralizedNewtypeDeriving hinges on the parameter's role being representational, but making it representational means users can also use coerce to turn dictionaries into other dictionaries outside of GND.

This is quite insidious, as another dictionary for Eq or Ord may exist for that type, where it becomes unsound as the generated dictionary may be used to destroy confluence. 

This means that even if something like Set has a nominal argument it isn't safe, because you can attack the invariants of the structure via Ord.

newtype Bad = Bad Int deriving Eq
instance Ord Bad where
   compare (Bad a) (Bad b) = compare b a

If Ord has a representational role then I can use coerce to convert a dictonary Ord Bad to Ord Int, then work locally in a context where that is the dictionary for Ord Int that I get when I go to do an insert or lookup.

I don't mean to sound like the sky is falling, but I do worry that the 'use of a constraint in a data type' may not be necessary or sufficient. That is a lot of surface area to defend against attack. 

I am not sure that I actually need a data type to coerce a dictionary. It seems likely that I could do it with just a well crafted function argument and ScopedTypeVariables, but my version of HEAD is a bit too mangled at the moment to give it a try.

-Edward


On Wed, Oct 9, 2013 at 2:09 PM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
I don't quite agree with your analysis, Edward.

Eq can be auto-derived, so it makes for a confusing example. Let's replace Eq in your example with this class:

> class C a where
>  c_meth :: a -> a -> Bool

Then, your example leads to the same embarrassing state of affairs: coercing a dictionary for (C Int) to one for (C Bar).

But, I would argue that we still want C's parameter to have a representational role. Why? Consider this:

> data Blargh = ...
> instance C Blargh where ...
>
> newtype Baz = MkBaz Blargh deriving C

We want that last line to work, using GeneralizedNewtypeDeriving. This hinges on C's parameter's role being representational.

I think that what you've witnessed is a case of bug #8338 (http://ghc.haskell.org/trac/ghc/ticket/8338). This is a problem, in my view, and it seems to touch on roles, but I'm not completely sure of their relationship.

So, I think that classes should keep their representational roles (regardless of the decision on datatypes -- Haskell doesn't really support "abstract" classes), but perhaps we have to find a way to stop these incoherent instances from forming. Maybe the use of a constraint makes a datatype's role be nominal?

Richard

On Oct 9, 2013, at 1:55 PM, Edward Kmett <ekmett <at> gmail.com> wrote:

I just noticed there is a pretty big issue with the current default role where typeclasses are concerned!

When implementing Data.Type.Coercion I had to use the fact that I could apply coerce to the arguments of

data Coercion a b where
  Coercion :: Coercible a b => Coercion a b

This makes sense as Coercion itself has two representational arguments.

This struck me as quite clever, so I went to test it further.

data Foo a where 
   Foo :: Eq a => Foo a

newtype Bar = Bar Int
instance Eq Bar where
  _ == _ = False

I fully expected the following to fail:

coerce (Foo :: Foo Int) :: Foo Bar

but instead it succeeded. 

This means I was able to convert a dictionary Eq Int into a dictionary for Eq Bar!

This indicates that Eq (actually all) of the typeclasses are currently marked as having representational, when actually it strikes me that (almost?) none of them should be.

Coercible is the only case I can think of in base of a class with two representational arguments, but this is only valid because we prevent users from defining Coercible instances manually.

If I try again with a new typeclass that has an explicit nominal role

type role Eq nominal
class Eq a
instance Eq Int
instance Eq Bar

then I get the failure to derive Coercible (Foo Int) (Foo Bar) that I'd expect.

This indicates two big issues to me: 

1.) At the very least the default role for type classes should be nominal for each argument. The very point of an instance is to make a nominal distinction after all. =)

2.) It also indicates that making any typeclass with a representational (/ phantom?) argument shouldn't be possible in valid SafeHaskell, as you can use it to subvert the current restrictions on OverlappingInstances.

-Edward


On Wed, Oct 9, 2013 at 12:07 PM, Iavor Diatchki <iavor.diatchki <at> gmail.com> wrote:
Hello,

My preference would be for the following design:

1. The default datatypes for roles are Nominal, but programmers can add annotations to relax this.
2. Generlized newtype deriving works as follows:  we can coerce a dictionary for `C R` into `C T`, as long as we can coerce the types of all methods instantiated with `R`, into the corresponding types instantiated with `T`.  In other words, we are pretending that we are implementing all methods by using `coerce`.

As far as I can see this safe, and matches what I'd expect as a programmer.  It also solves the problem with the `Set` example: because `Set` has a nominal parameter, we cannot coerce `Set Int` into `Set MyAge` and, hence, we cannot derive an instance of `MyAge` for `HasSet`.  An added benefit of this approach is that when newtype deriving fails, we can give a nicer error saying exactly which method causes the problem.

-Iavor






On Mon, Oct 7, 2013 at 6:26 AM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
As you may have heard, /roles/ will be introduced with GHC 7.8. Roles are a mechanism to allow for safe 0-cost conversions between newtypes and their base types. GeneralizedNewtypeDeriving (GND) already did this for class instances, but in an unsafe way -- the feature has essentially been retrofitted to work with roles. This means that some uses of GND that appear to be unsafe will no longer work. See the wiki page [1] or slides from a recent presentation [2] for more info.


I am writing because it's unclear what the *default* role should be -- that is, should GND be allowed by default? Examples follow, but the critical issue is this:

* If we allow GND by default anywhere it is type-safe, datatypes (even those that don't export constructors) will not be abstract by default. Library writers would have to use a role annotation everywhere they wish to declare a datatype they do not want users to be able to inspect. (Roles still keep type-*un*safe GND from happening.)

* If we disallow GND by default, then perhaps lots of current uses of GND will break. Library writers will have to explicitly declare when they wish to permit GND involving a datatype.

Which do we think is better?

Examples: The chief example demonstrating the problem is (a hypothetical implementation of) Set:

> module Set (Set) where   -- note: no constructors exported!
>
> data Set a = MkSet [a]
> insert :: Ord a => a -> Set a -> Set a
> ...

> {-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving #-}
> module Client where
>
> import Set
>
> newtype Age = MkAge Int deriving Eq
>
> instance Ord Age where
>   (MkAge a) `compare` (MkAge b) = b `compare` a   -- flip operands, reversing the order
>
> class HasSet a where
>   getSet :: Set a
>
> instance HasSet Int where
>   getSet = insert 2 (insert 5 empty)
>
> deriving instance HasSet Age
>
> good :: Set Int
> good = getSet
>
> bad :: Set Age
> bad = getSet

According to the way GND works, `good` and `bad` will have the same runtime representation. But, using Set operations on `bad` would indeed be bad -- because the Ord instance for Age is different than that for Int, Set operations will fail unexpectedly on `bad`. The problem is that Set should really be abstract, but we've been able to break this abstraction with GND. Note that there is no type error in these operations, just wrong behavior.

So, if we default to *no* GND, then the "deriving" line above would have an error and this problem wouldn't happen. If we default to *allowing* GND, then the writer of Set would have to include
> type role Set nominal
in the definition of the Set module to prevent the use of GND. (Why that peculiar annotation? See the linked further reading, above.)

Although it doesn't figure in this example, a library writer who wishes to allow GND in the default-no scenario would need a similar annotation
> type role Foo representational
to allow it.

There are clearly reasons for and against either decision, but which is better? Let the users decide!

Discussion time: 2 weeks.

Thanks!
Richard

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users



_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users




_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Richard Eisenberg | 9 Oct 21:21 2013

Re: default roles

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.

On Oct 9, 2013, at 2:52 PM, Edward Kmett <ekmett <at> gmail.com> wrote:

I'd be happy to be wrong. =)

We do seem to have stumbled into a design paradox though.

To make it so you can use roles in GeneralizedNewtypeDeriving hinges on the parameter's role being representational, but making it representational means users can also use coerce to turn dictionaries into other dictionaries outside of GND.

This is quite insidious, as another dictionary for Eq or Ord may exist for that type, where it becomes unsound as the generated dictionary may be used to destroy confluence. 

This means that even if something like Set has a nominal argument it isn't safe, because you can attack the invariants of the structure via Ord.

newtype Bad = Bad Int deriving Eq
instance Ord Bad where
   compare (Bad a) (Bad b) = compare b a

If Ord has a representational role then I can use coerce to convert a dictonary Ord Bad to Ord Int, then work locally in a context where that is the dictionary for Ord Int that I get when I go to do an insert or lookup.

I don't mean to sound like the sky is falling, but I do worry that the 'use of a constraint in a data type' may not be necessary or sufficient. That is a lot of surface area to defend against attack. 

I am not sure that I actually need a data type to coerce a dictionary. It seems likely that I could do it with just a well crafted function argument and ScopedTypeVariables, but my version of HEAD is a bit too mangled at the moment to give it a try.

-Edward


On Wed, Oct 9, 2013 at 2:09 PM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
I don't quite agree with your analysis, Edward.

Eq can be auto-derived, so it makes for a confusing example. Let's replace Eq in your example with this class:

> class C a where
>  c_meth :: a -> a -> Bool

Then, your example leads to the same embarrassing state of affairs: coercing a dictionary for (C Int) to one for (C Bar).

But, I would argue that we still want C's parameter to have a representational role. Why? Consider this:

> data Blargh = ...
> instance C Blargh where ...
>
> newtype Baz = MkBaz Blargh deriving C

We want that last line to work, using GeneralizedNewtypeDeriving. This hinges on C's parameter's role being representational.

I think that what you've witnessed is a case of bug #8338 (http://ghc.haskell.org/trac/ghc/ticket/8338). This is a problem, in my view, and it seems to touch on roles, but I'm not completely sure of their relationship.

So, I think that classes should keep their representational roles (regardless of the decision on datatypes -- Haskell doesn't really support "abstract" classes), but perhaps we have to find a way to stop these incoherent instances from forming. Maybe the use of a constraint makes a datatype's role be nominal?

Richard

On Oct 9, 2013, at 1:55 PM, Edward Kmett <ekmett <at> gmail.com> wrote:

I just noticed there is a pretty big issue with the current default role where typeclasses are concerned!

When implementing Data.Type.Coercion I had to use the fact that I could apply coerce to the arguments of

data Coercion a b where
  Coercion :: Coercible a b => Coercion a b

This makes sense as Coercion itself has two representational arguments.

This struck me as quite clever, so I went to test it further.

data Foo a where 
   Foo :: Eq a => Foo a

newtype Bar = Bar Int
instance Eq Bar where
  _ == _ = False

I fully expected the following to fail:

coerce (Foo :: Foo Int) :: Foo Bar

but instead it succeeded. 

This means I was able to convert a dictionary Eq Int into a dictionary for Eq Bar!

This indicates that Eq (actually all) of the typeclasses are currently marked as having representational, when actually it strikes me that (almost?) none of them should be.

Coercible is the only case I can think of in base of a class with two representational arguments, but this is only valid because we prevent users from defining Coercible instances manually.

If I try again with a new typeclass that has an explicit nominal role

type role Eq nominal
class Eq a
instance Eq Int
instance Eq Bar

then I get the failure to derive Coercible (Foo Int) (Foo Bar) that I'd expect.

This indicates two big issues to me: 

1.) At the very least the default role for type classes should be nominal for each argument. The very point of an instance is to make a nominal distinction after all. =)

2.) It also indicates that making any typeclass with a representational (/ phantom?) argument shouldn't be possible in valid SafeHaskell, as you can use it to subvert the current restrictions on OverlappingInstances.

-Edward


On Wed, Oct 9, 2013 at 12:07 PM, Iavor Diatchki <iavor.diatchki <at> gmail.com> wrote:
Hello,

My preference would be for the following design:

1. The default datatypes for roles are Nominal, but programmers can add annotations to relax this.
2. Generlized newtype deriving works as follows:  we can coerce a dictionary for `C R` into `C T`, as long as we can coerce the types of all methods instantiated with `R`, into the corresponding types instantiated with `T`.  In other words, we are pretending that we are implementing all methods by using `coerce`.

As far as I can see this safe, and matches what I'd expect as a programmer.  It also solves the problem with the `Set` example: because `Set` has a nominal parameter, we cannot coerce `Set Int` into `Set MyAge` and, hence, we cannot derive an instance of `MyAge` for `HasSet`.  An added benefit of this approach is that when newtype deriving fails, we can give a nicer error saying exactly which method causes the problem.

-Iavor






On Mon, Oct 7, 2013 at 6:26 AM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
As you may have heard, /roles/ will be introduced with GHC 7.8. Roles are a mechanism to allow for safe 0-cost conversions between newtypes and their base types. GeneralizedNewtypeDeriving (GND) already did this for class instances, but in an unsafe way -- the feature has essentially been retrofitted to work with roles. This means that some uses of GND that appear to be unsafe will no longer work. See the wiki page [1] or slides from a recent presentation [2] for more info.


I am writing because it's unclear what the *default* role should be -- that is, should GND be allowed by default? Examples follow, but the critical issue is this:

* If we allow GND by default anywhere it is type-safe, datatypes (even those that don't export constructors) will not be abstract by default. Library writers would have to use a role annotation everywhere they wish to declare a datatype they do not want users to be able to inspect. (Roles still keep type-*un*safe GND from happening.)

* If we disallow GND by default, then perhaps lots of current uses of GND will break. Library writers will have to explicitly declare when they wish to permit GND involving a datatype.

Which do we think is better?

Examples: The chief example demonstrating the problem is (a hypothetical implementation of) Set:

> module Set (Set) where   -- note: no constructors exported!
>
> data Set a = MkSet [a]
> insert :: Ord a => a -> Set a -> Set a
> ...

> {-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving #-}
> module Client where
>
> import Set
>
> newtype Age = MkAge Int deriving Eq
>
> instance Ord Age where
>   (MkAge a) `compare` (MkAge b) = b `compare` a   -- flip operands, reversing the order
>
> class HasSet a where
>   getSet :: Set a
>
> instance HasSet Int where
>   getSet = insert 2 (insert 5 empty)
>
> deriving instance HasSet Age
>
> good :: Set Int
> good = getSet
>
> bad :: Set Age
> bad = getSet

According to the way GND works, `good` and `bad` will have the same runtime representation. But, using Set operations on `bad` would indeed be bad -- because the Ord instance for Age is different than that for Int, Set operations will fail unexpectedly on `bad`. The problem is that Set should really be abstract, but we've been able to break this abstraction with GND. Note that there is no type error in these operations, just wrong behavior.

So, if we default to *no* GND, then the "deriving" line above would have an error and this problem wouldn't happen. If we default to *allowing* GND, then the writer of Set would have to include
> type role Set nominal
in the definition of the Set module to prevent the use of GND. (Why that peculiar annotation? See the linked further reading, above.)

Although it doesn't figure in this example, a library writer who wishes to allow GND in the default-no scenario would need a similar annotation
> type role Foo representational
to allow it.

There are clearly reasons for and against either decision, but which is better? Let the users decide!

Discussion time: 2 weeks.

Thanks!
Richard

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users



_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users





_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Joachim Breitner | 9 Oct 21:41 2013
Picon

Re: default roles

Hi,

Am Mittwoch, den 09.10.2013, 15:21 -0400 schrieb Richard Eisenberg:
> 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.

what do you need the extra bit for? During GHD, can’t you just create
the new dictionary (using "method = coerce original_method) and then see
if it typechecks, i.e. if the method types can be coerced.

(If not, the error messages might need massaging, though.)

Greetings,
Joachim

--

-- 
Joachim “nomeata” Breitner
  mail <at> joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nomeata <at> joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata <at> debian.org
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Edward Kmett | 9 Oct 21:41 2013
Picon

Re: default roles

On Wed, Oct 9, 2013 at 3:21 PM, Richard Eisenberg <eir <at> 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.)
 
=)
 
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 gehingt 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?

This strikes me as a remarkably straightforward solution. Does it strike you as something implementable in time for 7.8 though?

 
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.

Upon reflection it makes a lot of sense that GND has to mint a new dictionary, because the superclasses may differ, like you showed here.

-Edward
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Richard Eisenberg | 9 Oct 22:18 2013

Re: default roles


On Oct 9, 2013, at 3:41 PM, Joachim Breitner <mail <at> joachim-breitner.de> wrote:

> what do you need the extra bit for? During GHD, can’t you just create
> the new dictionary (using "method = coerce original_method) and then see
> if it typechecks, i.e. if the method types can be coerced.
> 
Efficiency. You're absolutely right -- you could just run the check at a use site of GND. I just thought it was
cleaner to talk about storing it.

On Oct 9, 2013, at 3:41 PM, Edward Kmett <ekmett <at> gmail.com> wrote:

> 
> This strikes me as a remarkably straightforward solution. Does it strike you as something implementable
in time for 7.8 though?
> 
>  

Yes. I imagine updating the documentation will be harder than updating the implementation, especially if
we go with Joachim's checking lazily idea -- that is, at the use site of GND instead of pre-calculating
whether GND would work. The error messages would be easy to get right, and might actually be more
informative than they currently are. Come to think of it, calculating this at the use site of GND is
probably preferable as it will improve error messages -- users will see exactly which feature of a class
makes it unsuitable for GND. This is a big improvement over the error message now.

And, just a slightly-cleverer-than-the-dumbest-possible test here would allow, say, GND to work with
(IArray UArray), a need which came up within GHC and with one of the failing packages on Hackage.

> 
> Upon reflection it makes a lot of sense that GND has to mint a new dictionary, because the superclasses may
differ, like you showed here.

Yes, of course. That's why it must be the way it is.

On Oct 9, 2013, at 3:44 PM, Edward Kmett <ekmett <at> gmail.com> wrote:

> The only class I'd want to preserve a representational roles for its arguments for would be Coercible.
> 
> It does strike me as interesting to consider what it would mean to properly check other instances for
overlap when the instances are defined only 'up to representation'.
> 
> It also strikes me as quite a rabbit hole. ;)

Perhaps if IncoherentInstances is on, classes get representational roles. This actually makes sense --
IncoherentInstances says not to care about coherence, and the nominal roles on classes are to enforce
coherence. The Coercible class is very incoherent (as in, *any* instance of the right type will work; we
don't care which one), and so it should have representational roles, according to this logic. This
default could be overridden by a type annotation, but I'm inclined *not* to let users override a class's
default nominal role with an annotation.

Richard
Joachim Breitner | 10 Oct 00:24 2013
Picon

Re: default roles

Hi,

not sure if this is not old news to you all, but I think that for this
discussion, it helps to consider these two aspects of a class instance
separately:
  (1) An instance is a record of functions
  (2) An instance is a function of sorts¹ from types to (1)
and clearly, type parameters of (1) can be representational, but the
function in (2) should have its parameters nominal.

Therefore it is fine to coerce the dictionary of a function (and would
we want to implement GND this ways, that would be fine), but not a type
involving a constraint.

Inside GHC, as far as I can tell, (2) exists in the form of the instance
metadata, and disappears after desugaring, while (1) is the actual
dictionary that exists in core as a regular data type.

So the conclusion is indeed: Let type class constraints have a nominal
role, and all is fine.

Greetings,
Joachim

¹ well, a kind of function. But not that type of kind, but the other
type. Sort of, at least.

--

-- 
Joachim “nomeata” Breitner
  mail <at> joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nomeata <at> joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata <at> debian.org
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Richard Eisenberg | 10 Oct 05:18 2013

Re: default roles


On Oct 9, 2013, at 6:24 PM, Joachim Breitner <mail <at> joachim-breitner.de> 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.

Richard
Joachim Breitner | 10 Oct 09:23 2013
Picon

Re: default roles

Hi,

Am Mittwoch, den 09.10.2013, 23:18 -0400 schrieb Richard Eisenberg:
> On Oct 9, 2013, at 6:24 PM, Joachim Breitner <mail <at> joachim-breitner.de> 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
  mail <at> joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nomeata <at> joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata <at> debian.org
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Edward Kmett | 9 Oct 21:44 2013
Picon

Re: default roles

The only class I'd want to preserve a representational roles for its arguments for would be Coercible.

It does strike me as interesting to consider what it would mean to properly check other instances for overlap when the instances are defined only 'up to representation'.

It also strikes me as quite a rabbit hole. ;)

-Edward


On Wed, Oct 9, 2013 at 3:21 PM, Richard Eisenberg <eir <at> 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.

On Oct 9, 2013, at 2:52 PM, Edward Kmett <ekmett <at> gmail.com> wrote:

I'd be happy to be wrong. =)

We do seem to have stumbled into a design paradox though.

To make it so you can use roles in GeneralizedNewtypeDeriving hinges on the parameter's role being representational, but making it representational means users can also use coerce to turn dictionaries into other dictionaries outside of GND.

This is quite insidious, as another dictionary for Eq or Ord may exist for that type, where it becomes unsound as the generated dictionary may be used to destroy confluence. 

This means that even if something like Set has a nominal argument it isn't safe, because you can attack the invariants of the structure via Ord.

newtype Bad = Bad Int deriving Eq
instance Ord Bad where
   compare (Bad a) (Bad b) = compare b a

If Ord has a representational role then I can use coerce to convert a dictonary Ord Bad to Ord Int, then work locally in a context where that is the dictionary for Ord Int that I get when I go to do an insert or lookup.

I don't mean to sound like the sky is falling, but I do worry that the 'use of a constraint in a data type' may not be necessary or sufficient. That is a lot of surface area to defend against attack. 

I am not sure that I actually need a data type to coerce a dictionary. It seems likely that I could do it with just a well crafted function argument and ScopedTypeVariables, but my version of HEAD is a bit too mangled at the moment to give it a try.

-Edward


On Wed, Oct 9, 2013 at 2:09 PM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
I don't quite agree with your analysis, Edward.

Eq can be auto-derived, so it makes for a confusing example. Let's replace Eq in your example with this class:

> class C a where
>  c_meth :: a -> a -> Bool

Then, your example leads to the same embarrassing state of affairs: coercing a dictionary for (C Int) to one for (C Bar).

But, I would argue that we still want C's parameter to have a representational role. Why? Consider this:

> data Blargh = ...
> instance C Blargh where ...
>
> newtype Baz = MkBaz Blargh deriving C

We want that last line to work, using GeneralizedNewtypeDeriving. This hinges on C's parameter's role being representational.

I think that what you've witnessed is a case of bug #8338 (http://ghc.haskell.org/trac/ghc/ticket/8338). This is a problem, in my view, and it seems to touch on roles, but I'm not completely sure of their relationship.

So, I think that classes should keep their representational roles (regardless of the decision on datatypes -- Haskell doesn't really support "abstract" classes), but perhaps we have to find a way to stop these incoherent instances from forming. Maybe the use of a constraint makes a datatype's role be nominal?

Richard

On Oct 9, 2013, at 1:55 PM, Edward Kmett <ekmett <at> gmail.com> wrote:

I just noticed there is a pretty big issue with the current default role where typeclasses are concerned!

When implementing Data.Type.Coercion I had to use the fact that I could apply coerce to the arguments of

data Coercion a b where
  Coercion :: Coercible a b => Coercion a b

This makes sense as Coercion itself has two representational arguments.

This struck me as quite clever, so I went to test it further.

data Foo a where 
   Foo :: Eq a => Foo a

newtype Bar = Bar Int
instance Eq Bar where
  _ == _ = False

I fully expected the following to fail:

coerce (Foo :: Foo Int) :: Foo Bar

but instead it succeeded. 

This means I was able to convert a dictionary Eq Int into a dictionary for Eq Bar!

This indicates that Eq (actually all) of the typeclasses are currently marked as having representational, when actually it strikes me that (almost?) none of them should be.

Coercible is the only case I can think of in base of a class with two representational arguments, but this is only valid because we prevent users from defining Coercible instances manually.

If I try again with a new typeclass that has an explicit nominal role

type role Eq nominal
class Eq a
instance Eq Int
instance Eq Bar

then I get the failure to derive Coercible (Foo Int) (Foo Bar) that I'd expect.

This indicates two big issues to me: 

1.) At the very least the default role for type classes should be nominal for each argument. The very point of an instance is to make a nominal distinction after all. =)

2.) It also indicates that making any typeclass with a representational (/ phantom?) argument shouldn't be possible in valid SafeHaskell, as you can use it to subvert the current restrictions on OverlappingInstances.

-Edward


On Wed, Oct 9, 2013 at 12:07 PM, Iavor Diatchki <iavor.diatchki <at> gmail.com> wrote:
Hello,

My preference would be for the following design:

1. The default datatypes for roles are Nominal, but programmers can add annotations to relax this.
2. Generlized newtype deriving works as follows:  we can coerce a dictionary for `C R` into `C T`, as long as we can coerce the types of all methods instantiated with `R`, into the corresponding types instantiated with `T`.  In other words, we are pretending that we are implementing all methods by using `coerce`.

As far as I can see this safe, and matches what I'd expect as a programmer.  It also solves the problem with the `Set` example: because `Set` has a nominal parameter, we cannot coerce `Set Int` into `Set MyAge` and, hence, we cannot derive an instance of `MyAge` for `HasSet`.  An added benefit of this approach is that when newtype deriving fails, we can give a nicer error saying exactly which method causes the problem.

-Iavor






On Mon, Oct 7, 2013 at 6:26 AM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
As you may have heard, /roles/ will be introduced with GHC 7.8. Roles are a mechanism to allow for safe 0-cost conversions between newtypes and their base types. GeneralizedNewtypeDeriving (GND) already did this for class instances, but in an unsafe way -- the feature has essentially been retrofitted to work with roles. This means that some uses of GND that appear to be unsafe will no longer work. See the wiki page [1] or slides from a recent presentation [2] for more info.


I am writing because it's unclear what the *default* role should be -- that is, should GND be allowed by default? Examples follow, but the critical issue is this:

* If we allow GND by default anywhere it is type-safe, datatypes (even those that don't export constructors) will not be abstract by default. Library writers would have to use a role annotation everywhere they wish to declare a datatype they do not want users to be able to inspect. (Roles still keep type-*un*safe GND from happening.)

* If we disallow GND by default, then perhaps lots of current uses of GND will break. Library writers will have to explicitly declare when they wish to permit GND involving a datatype.

Which do we think is better?

Examples: The chief example demonstrating the problem is (a hypothetical implementation of) Set:

> module Set (Set) where   -- note: no constructors exported!
>
> data Set a = MkSet [a]
> insert :: Ord a => a -> Set a -> Set a
> ...

> {-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving #-}
> module Client where
>
> import Set
>
> newtype Age = MkAge Int deriving Eq
>
> instance Ord Age where
>   (MkAge a) `compare` (MkAge b) = b `compare` a   -- flip operands, reversing the order
>
> class HasSet a where
>   getSet :: Set a
>
> instance HasSet Int where
>   getSet = insert 2 (insert 5 empty)
>
> deriving instance HasSet Age
>
> good :: Set Int
> good = getSet
>
> bad :: Set Age
> bad = getSet

According to the way GND works, `good` and `bad` will have the same runtime representation. But, using Set operations on `bad` would indeed be bad -- because the Ord instance for Age is different than that for Int, Set operations will fail unexpectedly on `bad`. The problem is that Set should really be abstract, but we've been able to break this abstraction with GND. Note that there is no type error in these operations, just wrong behavior.

So, if we default to *no* GND, then the "deriving" line above would have an error and this problem wouldn't happen. If we default to *allowing* GND, then the writer of Set would have to include
> type role Set nominal
in the definition of the Set module to prevent the use of GND. (Why that peculiar annotation? See the linked further reading, above.)

Although it doesn't figure in this example, a library writer who wishes to allow GND in the default-no scenario would need a similar annotation
> type role Foo representational
to allow it.

There are clearly reasons for and against either decision, but which is better? Let the users decide!

Discussion time: 2 weeks.

Thanks!
Richard

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users



_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users






_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
David Menendez | 10 Oct 17:24 2013

Re: default roles

On Wed, Oct 9, 2013 at 3:21 PM, Richard Eisenberg <eir <at> 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 <dave <at> zednenem.com>
<http://www.eyrie.org/~zednenem/>
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones | 10 Oct 18:11 2013
Picon

RE: default roles

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-bounces <at> haskell.org] On Behalf Of David Menendez
Sent: 10 October 2013 16:25
To: Richard Eisenberg
Cc: glasgow-haskell-users <at> haskell.org Mailing List; Simon Peyton-Jones
Subject: Re: default roles

 

On Wed, Oct 9, 2013 at 3:21 PM, Richard Eisenberg <eir <at> 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 <dave <at> zednenem.com>
<http://www.eyrie.org/~zednenem/>

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
David Menendez | 10 Oct 19:14 2013

Re: default roles

On Thu, Oct 10, 2013 at 12:11 PM, Simon Peyton-Jones <simonpj <at> microsoft.com> 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 <dave <at> zednenem.com>
<http://www.eyrie.org/~zednenem/>
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Richard Eisenberg | 11 Oct 03:52 2013

Re: default roles


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
Edward Kmett | 11 Oct 04:09 2013
Picon

Re: default roles

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 <eir <at> cis.upenn.edu> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Richard Eisenberg | 11 Oct 04:39 2013

Re: default roles

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
David Menendez | 11 Oct 18:33 2013

Re: default roles

On Thu, Oct 10, 2013 at 10:09 PM, Edward Kmett <ekmett <at> gmail.com> 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". =(

It seems like doing GND for an instance is okay as long as it's done for all the superclasses as well.

Alternately, what about keeping non-specialized versions of the instance code around? Like, if we have (in pseudocode):

    ordint :: OrdInstance Int
    fooint :: FooInstance Int
    ordbar :: OrdInstance Bar

instead of saying foobar = coerce fooint, we could use

    fooint_ordint :: OrdInstance Int -> FooInstance Int

and set foobar = coerce (foointordint (coerce ordbar)

That seems like it would be correct, albeit less efficient. We can still use coerce fooint for newtype of Int that also use GND for the Ord instance.

--
Dave Menendez <dave <at> zednenem.com>
<http://www.eyrie.org/~zednenem/>
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones | 11 Oct 19:00 2013
Picon

RE: default roles

Wait, that sounds like it induces bad semantics. 

 

I’m not sure this is as bad as you say.

 

First, in this case Set’s argument has nominal role, so the GND you give would be rejected anyway.  So Set’s sanctity stays unscathed.

 

But beyond that, when you say

newtype Bar = Bar Int deriving (Eq,Foo)

the “deriving Foo” bit says

 

“please implement all the Foo operations on Bar values in precisely the same way that you implement Foo operations on Int.”

 

Now that might be a stupid thing to say.  There are many ways in which it could be semantically wrong.  One of them is that Ints are ordered one way and Bars are ordered another.  But there may be other ways too.  Perhaps Bars have properties that Ints don’t which mean that inserting should work differently.  A type system cannot hope to catch all of these.

 

Simon

 

From: Edward Kmett [mailto:ekmett <at> gmail.com]
Sent: 11 October 2013 03:09
To: Richard Eisenberg
Cc: David Menendez; glasgow-haskell-users <at> haskell.org Mailing List; Simon Peyton-Jones
Subject: Re: default roles

 

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 <eir <at> cis.upenn.edu> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

 

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Edward Kmett | 11 Oct 19:58 2013
Picon

Re: default roles

On Fri, Oct 11, 2013 at 1:00 PM, Simon Peyton-Jones <simonpj <at> microsoft.com> wrote:

First, in this case Set’s argument has nominal role, so the GND you give would be rejected anyway.  So Set’s sanctity stays unscathed.

Fair enough. I'm very happy to hear that avenue of attack doesn't work. =)

But beyond that, when you say

newtype Bar = Bar Int deriving (Eq,Foo)

the “deriving Foo” bit says 

“please implement all the Foo operations on Bar values in precisely the same way that you implement Foo operations on Int.”

Now that might be a stupid thing to say.  There are many ways in which it could be semantically wrong.  One of them is that Ints are ordered one way and Bars are ordered another.  But there may be other ways too.  Perhaps Bars have properties that Ints don’t which mean that inserting should work differently.  A type system cannot hope to catch all of these.


My main concern is just making sure that we don't wind up with situations where you can get two instances of, say, Eq Bar that disagree under Safe Haskell depending on where you obtained it.

So far Richard's proposed fix has handled every attack I've come up with. I'll go back to looking for other attack vectors.

-Edward
 

From: Edward Kmett [mailto:ekmett <at> gmail.com]
Sent: 11 October 2013 03:09
To: Richard Eisenberg
Cc: David Menendez; glasgow-haskell-users <at> haskell.org Mailing List; Simon Peyton-Jones
Subject: Re: default roles

 

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 <eir <at> cis.upenn.edu> 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 <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

 


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones | 10 Oct 11:49 2013
Picon

RE: default roles

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.)

 

Yes, this seems right.  And NOW I finally realise why GHC implements GND like this.  Consider

 

  class Show a => C a where { op :: a -> a }

  instance C Int where …

  newtype Age = Age Int deriving( Show, C )

 

Here we want to make a (C Age) dictionary that use the (C Int) version of ‘op’.  But the superclass for (Show Age) must not use the (Show Int) version of ‘show’!  It must use Age’s own version of Show.

 

So we I think Richard’s proposal is spot on.  Go for it.   Can you work on that, Richard?


Simon

 

From: Glasgow-haskell-users [mailto:glasgow-haskell-users-bounces <at> haskell.org] On Behalf Of Richard Eisenberg
Sent: 09 October 2013 20:21
To: Edward Kmett
Cc: Simon Peyton-Jones; glasgow-haskell-users <at> haskell.org Mailing List
Subject: Re: default roles

 

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.

 

On Oct 9, 2013, at 2:52 PM, Edward Kmett <ekmett <at> gmail.com> wrote:



I'd be happy to be wrong. =)

 

We do seem to have stumbled into a design paradox though.

 

To make it so you can use roles in GeneralizedNewtypeDeriving hinges on the parameter's role being representational, but making it representational means users can also use coerce to turn dictionaries into other dictionaries outside of GND.

 

This is quite insidious, as another dictionary for Eq or Ord may exist for that type, where it becomes unsound as the generated dictionary may be used to destroy confluence. 

 

This means that even if something like Set has a nominal argument it isn't safe, because you can attack the invariants of the structure via Ord.

 

newtype Bad = Bad Int deriving Eq

instance Ord Bad where

   compare (Bad a) (Bad b) = compare b a

 

If Ord has a representational role then I can use coerce to convert a dictonary Ord Bad to Ord Int, then work locally in a context where that is the dictionary for Ord Int that I get when I go to do an insert or lookup.

 

I don't mean to sound like the sky is falling, but I do worry that the 'use of a constraint in a data type' may not be necessary or sufficient. That is a lot of surface area to defend against attack. 

 

I am not sure that I actually need a data type to coerce a dictionary. It seems likely that I could do it with just a well crafted function argument and ScopedTypeVariables, but my version of HEAD is a bit too mangled at the moment to give it a try.

 

-Edward

 

On Wed, Oct 9, 2013 at 2:09 PM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:

I don't quite agree with your analysis, Edward.

 

Eq can be auto-derived, so it makes for a confusing example. Let's replace Eq in your example with this class:

 

> class C a where

>  c_meth :: a -> a -> Bool

 

Then, your example leads to the same embarrassing state of affairs: coercing a dictionary for (C Int) to one for (C Bar).

 

But, I would argue that we still want C's parameter to have a representational role. Why? Consider this:

 

> data Blargh = ...

> instance C Blargh where ...

>

 

> newtype Baz = MkBaz Blargh deriving C

 

We want that last line to work, using GeneralizedNewtypeDeriving. This hinges on C's parameter's role being representational.

 

I think that what you've witnessed is a case of bug #8338 (http://ghc.haskell.org/trac/ghc/ticket/8338). This is a problem, in my view, and it seems to touch on roles, but I'm not completely sure of their relationship.

 

So, I think that classes should keep their representational roles (regardless of the decision on datatypes -- Haskell doesn't really support "abstract" classes), but perhaps we have to find a way to stop these incoherent instances from forming. Maybe the use of a constraint makes a datatype's role be nominal?

 

Richard

 

On Oct 9, 2013, at 1:55 PM, Edward Kmett <ekmett <at> gmail.com> wrote:



I just noticed there is a pretty big issue with the current default role where typeclasses are concerned!

 

When implementing Data.Type.Coercion I had to use the fact that I could apply coerce to the arguments of

 

data Coercion a b where

  Coercion :: Coercible a b => Coercion a b

 

This makes sense as Coercion itself has two representational arguments.

 

This struck me as quite clever, so I went to test it further.

 

data Foo a where 

   Foo :: Eq a => Foo a

 

newtype Bar = Bar Int

instance Eq Bar where

  _ == _ = False

 

I fully expected the following to fail:

 

coerce (Foo :: Foo Int) :: Foo Bar

 

but instead it succeeded. 

 

This means I was able to convert a dictionary Eq Int into a dictionary for Eq Bar!

 

This indicates that Eq (actually all) of the typeclasses are currently marked as having representational, when actually it strikes me that (almost?) none of them should be.

 

Coercible is the only case I can think of in base of a class with two representational arguments, but this is only valid because we prevent users from defining Coercible instances manually.

 

If I try again with a new typeclass that has an explicit nominal role

 

type role Eq nominal

class Eq a

instance Eq Int

instance Eq Bar

 

then I get the failure to derive Coercible (Foo Int) (Foo Bar) that I'd expect.

 

This indicates two big issues to me: 

 

1.) At the very least the default role for type classes should be nominal for each argument. The very point of an instance is to make a nominal distinction after all. =)

 

2.) It also indicates that making any typeclass with a representational (/ phantom?) argument shouldn't be possible in valid SafeHaskell, as you can use it to subvert the current restrictions on OverlappingInstances.

 

-Edward

 

On Wed, Oct 9, 2013 at 12:07 PM, Iavor Diatchki <iavor.diatchki <at> gmail.com> wrote:

Hello,

 

My preference would be for the following design:

 

1. The default datatypes for roles are Nominal, but programmers can add annotations to relax this.

2. Generlized newtype deriving works as follows:  we can coerce a dictionary for `C R` into `C T`, as long as we can coerce the types of all methods instantiated with `R`, into the corresponding types instantiated with `T`.  In other words, we are pretending that we are implementing all methods by using `coerce`.

 

As far as I can see this safe, and matches what I'd expect as a programmer.  It also solves the problem with the `Set` example: because `Set` has a nominal parameter, we cannot coerce `Set Int` into `Set MyAge` and, hence, we cannot derive an instance of `MyAge` for `HasSet`.  An added benefit of this approach is that when newtype deriving fails, we can give a nicer error saying exactly which method causes the problem.

 

-Iavor

 

 

 

 

 

On Mon, Oct 7, 2013 at 6:26 AM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:

As you may have heard, /roles/ will be introduced with GHC 7.8. Roles are a mechanism to allow for safe 0-cost conversions between newtypes and their base types. GeneralizedNewtypeDeriving (GND) already did this for class instances, but in an unsafe way -- the feature has essentially been retrofitted to work with roles. This means that some uses of GND that appear to be unsafe will no longer work. See the wiki page [1] or slides from a recent presentation [2] for more info.

 

 

I am writing because it's unclear what the *default* role should be -- that is, should GND be allowed by default? Examples follow, but the critical issue is this:

 

* If we allow GND by default anywhere it is type-safe, datatypes (even those that don't export constructors) will not be abstract by default. Library writers would have to use a role annotation everywhere they wish to declare a datatype they do not want users to be able to inspect. (Roles still keep type-*un*safe GND from happening.)

 

* If we disallow GND by default, then perhaps lots of current uses of GND will break. Library writers will have to explicitly declare when they wish to permit GND involving a datatype.

 

Which do we think is better?

 

Examples: The chief example demonstrating the problem is (a hypothetical implementation of) Set:

 

> module Set (Set) where   -- note: no constructors exported!

>

 

> data Set a = MkSet [a]

> insert :: Ord a => a -> Set a -> Set a

> ...

 

> {-# LANGUAGE GeneralizedNewtypeDeriving, StandaloneDeriving #-}

> module Client where

>

 

> import Set

>

 

> newtype Age = MkAge Int deriving Eq

>

 

> instance Ord Age where

>   (MkAge a) `compare` (MkAge b) = b `compare` a   -- flip operands, reversing the order

>

 

> class HasSet a where

>   getSet :: Set a

>

 

> instance HasSet Int where

>   getSet = insert 2 (insert 5 empty)

>

 

> deriving instance HasSet Age

>

 

> good :: Set Int

> good = getSet

>

 

> bad :: Set Age

> bad = getSet

 

According to the way GND works, `good` and `bad` will have the same runtime representation. But, using Set operations on `bad` would indeed be bad -- because the Ord instance for Age is different than that for Int, Set operations will fail unexpectedly on `bad`. The problem is that Set should really be abstract, but we've been able to break this abstraction with GND. Note that there is no type error in these operations, just wrong behavior.

 

So, if we default to *no* GND, then the "deriving" line above would have an error and this problem wouldn't happen. If we default to *allowing* GND, then the writer of Set would have to include

> type role Set nominal

in the definition of the Set module to prevent the use of GND. (Why that peculiar annotation? See the linked further reading, above.)

 

Although it doesn't figure in this example, a library writer who wishes to allow GND in the default-no scenario would need a similar annotation

> type role Foo representational

to allow it.

 

There are clearly reasons for and against either decision, but which is better? Let the users decide!

 

Discussion time: 2 weeks.

 

Thanks!

Richard

 

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

 


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

 

 

 

 

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Gmane