Re: Proposal: GHC.Generics marked UNSAFE for SafeHaskell

newer
Back to explicit Coercible...

older
Status update on overloaded...

José Pedro Magalhães

8 Oct 2013 8 Oct '13

3:48 a.m.

Hi, On Mon, Oct 7, 2013 at 10:32 AM, Dag Odenhall wrote:

...

Here‘s a thought: doesn’t Generic already have an unused phantom type that's only there “just in case we need to add something in the future”?

No, it doesn't. Just a thought: what if we had a type family type family Derives (t :: k1) (c :: k2) :: Bool which would automatically be instantiated by GHC appropriately? E.g., if the user had the following code: data MyData = MyData deriving (Eq, Generic) deriving instance Show MyData instance Ord MyData GHC would automatically instantiate: type instance Derives MyData Eq = True type instance Derives MyData Generic = True type instance Derives MyData Show = True type instance Derives MyData Ord = False Would this be something Ryan could use for detecting safe instances for LVish? Cheers, Pedro

Attachments:

attachment.html (text/html — 2.0 KB)

Show replies by date

Ryan Newton

14 Oct 14 Oct

11:02 p.m.

New subject: Proposal: GHC.Generics marked UNSAFE for SafeHaskell

Hey, that's an awesome formulation! Thanks Pedro. Any idea how much work this would be to implement in GHC, if it did garner approval? On Tue, Oct 8, 2013 at 3:48 AM, José Pedro Magalhães wrote:

...

Hi,

On Mon, Oct 7, 2013 at 10:32 AM, Dag Odenhall wrote:

...
Here‘s a thought: doesn’t Generic already have an unused phantom type that's only there “just in case we need to add something in the future”?

No, it doesn't.

Just a thought: what if we had a type family

type family Derives (t :: k1) (c :: k2) :: Bool

which would automatically be instantiated by GHC appropriately? E.g., if the user had the following code:

data MyData = MyData deriving (Eq, Generic) deriving instance Show MyData instance Ord MyData

GHC would automatically instantiate:

type instance Derives MyData Eq = True type instance Derives MyData Generic = True type instance Derives MyData Show = True type instance Derives MyData Ord = False

Would this be something Ryan could use for detecting safe instances for LVish?

Cheers, Pedro

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

Nicolas Frisby

11:20 p.m.

New subject: Proposal: GHC.Generics marked UNSAFE for SafeHaskell

The formulation as a type family seems to conflict with the open-world principle. Would a class-based encoding instead be sufficient? -- the proposed, special wired-in class class Derives (t :: k1) (c :: k2) -- GHC would infer these from Pedro's example's declarations instance Derives MyData Eq instance Derives MyData Generic instance Derives MyData Show NB that there is no instance Derives MyData Ord, but standalone deriving could yield one "later" On Mon, Oct 14, 2013 at 10:02 PM, Ryan Newton wrote:

...

Hey, that's an awesome formulation! Thanks Pedro.

Any idea how much work this would be to implement in GHC, if it did garner approval?

On Tue, Oct 8, 2013 at 3:48 AM, José Pedro Magalhães wrote:

...
Hi,

On Mon, Oct 7, 2013 at 10:32 AM, Dag Odenhall wrote:

...
Here‘s a thought: doesn’t Generic already have an unused phantom type that's only there “just in case we need to add something in the future”?

No, it doesn't.

Just a thought: what if we had a type family

type family Derives (t :: k1) (c :: k2) :: Bool

which would automatically be instantiated by GHC appropriately? E.g., if the user had the following code:

data MyData = MyData deriving (Eq, Generic) deriving instance Show MyData instance Ord MyData

GHC would automatically instantiate:

type instance Derives MyData Eq = True type instance Derives MyData Generic = True type instance Derives MyData Show = True type instance Derives MyData Ord = False

Would this be something Ryan could use for detecting safe instances for LVish?

Cheers, Pedro

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

Ryan Newton

11:41 p.m.

New subject: Proposal: GHC.Generics marked UNSAFE for SafeHaskell

But what stops the user from defining their own instances if they in fact did not derive it? The explicit "False" in Pedro's formulation seems to serve this purpose. On Mon, Oct 14, 2013 at 11:20 PM, Nicolas Frisby wrote:

...

The formulation as a type family seems to conflict with the open-world principle. Would a class-based encoding instead be sufficient?

-- the proposed, special wired-in class class Derives (t :: k1) (c :: k2)

-- GHC would infer these from Pedro's example's declarations instance Derives MyData Eq instance Derives MyData Generic instance Derives MyData Show

NB that there is no instance Derives MyData Ord, but standalone deriving could yield one "later"

On Mon, Oct 14, 2013 at 10:02 PM, Ryan Newton wrote:

...
Hey, that's an awesome formulation! Thanks Pedro.

Any idea how much work this would be to implement in GHC, if it did garner approval?

On Tue, Oct 8, 2013 at 3:48 AM, José Pedro Magalhães wrote:

...
Hi,

On Mon, Oct 7, 2013 at 10:32 AM, Dag Odenhall wrote:

...
Here‘s a thought: doesn’t Generic already have an unused phantom type that's only there “just in case we need to add something in the future”?

No, it doesn't.

Just a thought: what if we had a type family

type family Derives (t :: k1) (c :: k2) :: Bool

which would automatically be instantiated by GHC appropriately? E.g., if the user had the following code:

data MyData = MyData deriving (Eq, Generic) deriving instance Show MyData instance Ord MyData

GHC would automatically instantiate:

type instance Derives MyData Eq = True type instance Derives MyData Generic = True type instance Derives MyData Show = True type instance Derives MyData Ord = False

Would this be something Ryan could use for detecting safe instances for LVish?

Cheers, Pedro

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

Edward Kmett

11:49 p.m.

New subject: Proposal: GHC.Generics marked UNSAFE for SafeHaskell

The issue with such an explicit false is that it requires more magic on behalf of the compiler. It would have to be filled in whenever an explicit `instance Eq Blah` was written. Recall that deriving instance Eq Blah can occur after the data type declaration site and may have to be used for many more complicated recursive data types, so it isn't sufficient to fill in at the data type declaration. -Edward On Mon, Oct 14, 2013 at 11:41 PM, Ryan Newton wrote:

...

But what stops the user from defining their own instances if they in fact did not derive it?

The explicit "False" in Pedro's formulation seems to serve this purpose.

On Mon, Oct 14, 2013 at 11:20 PM, Nicolas Frisby
...
wrote:

...
The formulation as a type family seems to conflict with the open-world principle. Would a class-based encoding instead be sufficient?

-- the proposed, special wired-in class class Derives (t :: k1) (c :: k2)

-- GHC would infer these from Pedro's example's declarations instance Derives MyData Eq instance Derives MyData Generic instance Derives MyData Show

NB that there is no instance Derives MyData Ord, but standalone deriving could yield one "later"

On Mon, Oct 14, 2013 at 10:02 PM, Ryan Newton wrote:

...
Hey, that's an awesome formulation! Thanks Pedro.

Any idea how much work this would be to implement in GHC, if it did garner approval?

On Tue, Oct 8, 2013 at 3:48 AM, José Pedro Magalhães wrote:

...
Hi,

On Mon, Oct 7, 2013 at 10:32 AM, Dag Odenhall wrote:

...
Here‘s a thought: doesn’t Generic already have an unused phantom type that's only there “just in case we need to add something in the future”?

No, it doesn't.

Just a thought: what if we had a type family

type family Derives (t :: k1) (c :: k2) :: Bool

which would automatically be instantiated by GHC appropriately? E.g., if the user had the following code:

data MyData = MyData deriving (Eq, Generic) deriving instance Show MyData instance Ord MyData

GHC would automatically instantiate:

type instance Derives MyData Eq = True type instance Derives MyData Generic = True type instance Derives MyData Show = True type instance Derives MyData Ord = False

Would this be something Ryan could use for detecting safe instances for LVish?

Cheers, Pedro

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

José Pedro Magalhães

15 Oct 15 Oct

8:28 a.m.

New subject: Proposal: GHC.Generics marked UNSAFE for SafeHaskell

On Tue, Oct 15, 2013 at 4:49 AM, Edward Kmett wrote:

...

The issue with such an explicit false is that it requires more magic on behalf of the compiler.

It would have to be filled in whenever an explicit `instance Eq Blah` was written.

Recall that

deriving instance Eq Blah

can occur after the data type declaration site and may have to be used for many more complicated recursive data types, so it isn't sufficient to fill in at the data type declaration.

Yes, I know. But I don't think this would require _more_ magic than the class instances. And I don't see how class instances solve the problem; how can the user be prevented from defining an |instance Derives MyData Eq| if the instance wasn't indeed derived? Only through compiler magic... Pedro

...

-Edward

On Mon, Oct 14, 2013 at 11:41 PM, Ryan Newton wrote:

...
But what stops the user from defining their own instances if they in fact did not derive it?

The explicit "False" in Pedro's formulation seems to serve this purpose.

On Mon, Oct 14, 2013 at 11:20 PM, Nicolas Frisby < nicolas.frisby@gmail.com> wrote:

...
The formulation as a type family seems to conflict with the open-world principle. Would a class-based encoding instead be sufficient?

-- the proposed, special wired-in class class Derives (t :: k1) (c :: k2)

-- GHC would infer these from Pedro's example's declarations instance Derives MyData Eq instance Derives MyData Generic instance Derives MyData Show

NB that there is no instance Derives MyData Ord, but standalone deriving could yield one "later"

On Mon, Oct 14, 2013 at 10:02 PM, Ryan Newton wrote:

...
Hey, that's an awesome formulation! Thanks Pedro.

Any idea how much work this would be to implement in GHC, if it did garner approval?

On Tue, Oct 8, 2013 at 3:48 AM, José Pedro Magalhães
...
wrote:

...
Hi,

On Mon, Oct 7, 2013 at 10:32 AM, Dag Odenhall wrote:

...
Here‘s a thought: doesn’t Generic already have an unused phantom type that's only there “just in case we need to add something in the future”?

No, it doesn't.

Just a thought: what if we had a type family

type family Derives (t :: k1) (c :: k2) :: Bool

which would automatically be instantiated by GHC appropriately? E.g., if the user had the following code:

data MyData = MyData deriving (Eq, Generic) deriving instance Show MyData instance Ord MyData

GHC would automatically instantiate:

type instance Derives MyData Eq = True type instance Derives MyData Generic = True type instance Derives MyData Show = True type instance Derives MyData Ord = False

Would this be something Ryan could use for detecting safe instances for LVish?

Cheers, Pedro

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

Nicolas Frisby

10:19 a.m.

New subject: Proposal: GHC.Generics marked UNSAFE for SafeHaskell

Ah, I see. I had implicitly assumed we were talking about yet another "magic" class. This is snow balling in my head right now, so I'll hold off on further suggestions. My main concern was the relationship between: * an irreducible application of the Derives type family * an application that reduces to False * an insoluble constraint for the Derives class On Oct 15, 2013 7:28 AM, "José Pedro Magalhães" wrote:

...

On Tue, Oct 15, 2013 at 4:49 AM, Edward Kmett wrote:

...
The issue with such an explicit false is that it requires more magic on behalf of the compiler.

It would have to be filled in whenever an explicit `instance Eq Blah` was written.

Recall that

deriving instance Eq Blah

can occur after the data type declaration site and may have to be used for many more complicated recursive data types, so it isn't sufficient to fill in at the data type declaration.

Yes, I know. But I don't think this would require _more_ magic than the class instances. And I don't see how class instances solve the problem; how can the user be prevented from defining an |instance Derives MyData Eq| if the instance wasn't indeed derived? Only through compiler magic...

Pedro

...
-Edward

On Mon, Oct 14, 2013 at 11:41 PM, Ryan Newton wrote:

...
But what stops the user from defining their own instances if they in fact did not derive it?

The explicit "False" in Pedro's formulation seems to serve this purpose.

On Mon, Oct 14, 2013 at 11:20 PM, Nicolas Frisby < nicolas.frisby@gmail.com> wrote:

...
The formulation as a type family seems to conflict with the open-world principle. Would a class-based encoding instead be sufficient?

-- the proposed, special wired-in class class Derives (t :: k1) (c :: k2)

-- GHC would infer these from Pedro's example's declarations instance Derives MyData Eq instance Derives MyData Generic instance Derives MyData Show

NB that there is no instance Derives MyData Ord, but standalone deriving could yield one "later"

On Mon, Oct 14, 2013 at 10:02 PM, Ryan Newton wrote:

...
Hey, that's an awesome formulation! Thanks Pedro.

Any idea how much work this would be to implement in GHC, if it did garner approval?

On Tue, Oct 8, 2013 at 3:48 AM, José Pedro Magalhães < dreixel@gmail.com> wrote:

...
Hi,

On Mon, Oct 7, 2013 at 10:32 AM, Dag Odenhall wrote:

> Here‘s a thought: doesn’t Generic already have an unused phantom > type that's only there “just in case we need to add something in the > future”? > No, it doesn't.

Just a thought: what if we had a type family

type family Derives (t :: k1) (c :: k2) :: Bool

which would automatically be instantiated by GHC appropriately? E.g., if the user had the following code:

data MyData = MyData deriving (Eq, Generic) deriving instance Show MyData instance Ord MyData

GHC would automatically instantiate:

type instance Derives MyData Eq = True type instance Derives MyData Generic = True type instance Derives MyData Show = True type instance Derives MyData Ord = False

Would this be something Ryan could use for detecting safe instances for LVish?

Cheers, Pedro

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________ Libraries mailing list Libraries@haskell.org http://www.haskell.org/mailman/listinfo/libraries

Simon Peyton-Jones

16 Oct 16 Oct

7:49 a.m.

New subject: Proposal: GHC.Generics marked UNSAFE for SafeHaskell

We have a constraint (a~b) that can appear in a type signature f :: (a~b) => a -> b We can also have a type-level equality function type family Eq a b where Eq a a = True Eq a b = False The type-level Boolean reflects the (a~b) constraint precisely. You sound as if you want a type family Satisfied, so you type family Satisfied :: Constraint -> Bool Then you could have instance Ord T where ... type instance Satisfied (Ord T) = True The difficulty is that we can never return False, because you can always make T an instance of Ord "later". And you can't have Satisfied (Ord T) returning True in one place and Falsie in another. It can get stuck (not reduce) but it can't return False. I don't know if this would be useful to you. And for more complex instances lie instance Ord a => Ord [a] I don't know what you want to say for type instance Satisfied (Ord a) = ??? Simon From: Libraries [mailto:libraries-bounces@haskell.org] On Behalf Of Ryan Newton Sent: 15 October 2013 04:03 To: Pedro Magalhães (dreixel@gmail.com) Cc: Haskell Libraries; Andres Löh; Ganesh Sittampalam; ghc-devs@haskell.org Subject: Re: Proposal: GHC.Generics marked UNSAFE for SafeHaskell Hey, that's an awesome formulation! Thanks Pedro. Any idea how much work this would be to implement in GHC, if it did garner approval? On Tue, Oct 8, 2013 at 3:48 AM, José Pedro Magalhães mailto:dreixel@gmail.com> wrote: Hi, On Mon, Oct 7, 2013 at 10:32 AM, Dag Odenhall mailto:dag.odenhall@gmail.com> wrote: Here's a thought: doesn't Generic already have an unused phantom type that's only there "just in case we need to add something in the future"? No, it doesn't. Just a thought: what if we had a type family type family Derives (t :: k1) (c :: k2) :: Bool which would automatically be instantiated by GHC appropriately? E.g., if the user had the following code: data MyData = MyData deriving (Eq, Generic) deriving instance Show MyData instance Ord MyData GHC would automatically instantiate: type instance Derives MyData Eq = True type instance Derives MyData Generic = True type instance Derives MyData Show = True type instance Derives MyData Ord = False Would this be something Ryan could use for detecting safe instances for LVish? Cheers, Pedro _______________________________________________ ghc-devs mailing list ghc-devs@haskell.orgmailto:ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

4237

Age (days ago)

4245

Last active (days ago)

List overview

Download

7 comments

5 participants

participants (5)

Edward Kmett
José Pedro Magalhães
Nicolas Frisby
Ryan Newton
Simon Peyton-Jones

Re: Proposal: GHC.Generics marked UNSAFE for SafeHaskell

tags

participants (5)