Peyton-Jones; glasgow-haskell-users@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
On Thu, Oct 10, 2013 at 10:09 PM, Edward Kmett ekm...@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 =
Hi,
Am Mittwoch, den 09.10.2013, 23:18 -0400 schrieb Richard Eisenberg:
On Oct 9, 2013, at 6:24 PM, Joachim Breitner m...@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
On Wed, Oct 9, 2013 at 3:21 PM, Richard Eisenberg e...@cis.upenn.edu wrote:
Now I think we're on the same page, and I *am* a little worried about the
sky falling because of this. (That's not a euphemism -- I'm only a little
worried.)
Well, maybe I should be more worried.
The whole idea of
On Thu, Oct 10, 2013 at 12:11 PM, Simon Peyton-Jones
simo...@microsoft.comwrote:
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
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
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 =
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
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
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
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
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
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
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
On Wed, Oct 9, 2013 at 3:21 PM, Richard Eisenberg e...@cis.upenn.edu wrote:
Now I think we're on the same page, and I *am* a little worried about the
sky falling because of this. (That's not a euphemism -- I'm only a little
worried.)
=)
Wait! I have an idea!
The way I've been describing
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
On Oct 9, 2013, at 3:41 PM, Joachim Breitner m...@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.
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)
On Oct 9, 2013, at 6:24 PM, Joachim Breitner m...@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
Hi,
On Tue, Oct 8, 2013 at 3:21 AM, Richard Eisenberg e...@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
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
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
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
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
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,
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
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.
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,
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
29 matches
Mail list logo
