Opened 6 years ago

Closed 3 years ago

Last modified 18 months ago

#8165 closed feature request (fixed)

Use GeneralizedNewtypeDeriving to automatically create associated type families

Reported by: MikeIzbicki Owned by: RyanGlScott
Priority: normal Milestone: 8.2.1
Component: Compiler (Type checker) Version: 7.6.3
Keywords: TypeFamilies, deriving Cc: RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: deriving/should_compile/T8165, deriving/should_fail/T8165_fail1, deriving/should_fail/T8165_fail2
Blocked By: Blocking:
Related Tickets: #2721 Differential Rev(s): Phab:D2636
Wiki Page:

Description

Here's a simple example:

class C a where
    type T a

instance C Int where
    type T Int = Bool

newtype NT = NT Int
    deriving C

Change History (25)

comment:1 Changed 6 years ago by goldfire

What should happen in this scenario:

class D a where
  type U a

instance D Int where
  type U Int = Int

newtype E = MkE Int
  deriving D

What does U E reduce to, E or Int?

comment:2 Changed 6 years ago by MikeIzbicki

Ambiguous cases like this could remain a type error. That would probably prevent the most confusion.

comment:3 in reply to:  2 Changed 6 years ago by MikeIzbicki

In all the cases where I've wanted to use this, the type is polymorphic. Here's a real example of when I've wanted to use this:

class HasRing a where
    type Ring a

instance HasRing [a] where type Ring [a] = a
instance Hasring (Vector a) where type Ring (Vector a) = a

newtype L2Norm a = L2Norm a
    deriving HasRing

newtype L1Norm a = L1Norm a
    deriving HasRing

The deriving clauses would be equivalent to:

instance HasRing a => HasRing (L2Norm a) where
    type Ring (L2Norm a) = Ring a

instance HasRing a => HasRing (L1Norm a) where
    type Ring (L1Norm a) = Ring a

This might become problematic if there are multiple type parameters though.

comment:4 Changed 6 years ago by goldfire

This auto-generation seems to be rather different from the way GeneralizedNewtypeDeriving works in other contexts. In particular, the instances that you're generating are not directly related to any existing instances. Are you proposing that type families used on derived instances should just "look through" the newtype and be applied to the base type? Or only in cases with type variables? And, where does the HasRing a => constraint come from?

Without those constraints, I can see more of a coherent and general picture here... but it doesn't seem like GeneralizedNewtypeDeriving to me. Perhaps you're really proposing a new extension for generation of type family instances for newtypes?

comment:5 Changed 5 years ago by thomie

Component: CompilerCompiler (Type checker)

comment:6 Changed 5 years ago by goldfire

Milestone: 7.12.1
Owner: set to goldfire

Encouraged by Iavor Diatchki and Adam Gundry, I've realized that my comment:4 is utterly wrong -- MikeIzbicki's proposal is reasonable.

Concretely, I propose:

  • GeneralizedNewtypeDeriving for classes with associated types define new associated type instances that "look through" to the underlying type instance.

This satisfies Mike's original example. To my comment:1, it says Int. And, this proposal works for comment:3.

Note that associated data instances will still be prohibited -- these are not covered by this ticket.

I can implement in due course.

comment:7 Changed 5 years ago by simonpj

So, to be more specific, the recipe is this:

class C a where
  type T a
  op :: a -> a

newtype T a = MkT <rep-type> deriving( C )

Here the deriving clause would generate

instance C <rep-type> => C (T a) where
  type T (T a) = T <rep-type>
  op = coerce (op :: <rep-type> -> <rep-type>)

As usual, a wiki page to explain the details when we have to eta-reduce the newtype, etc, would be helpful.

Simon

Version 0, edited 5 years ago by simonpj (next)

comment:8 Changed 4 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:9 Changed 4 years ago by RyanGlScott

Would this approach be able to work for associated injective type families? If you had something like this:

class C a where
  type T a = r | r -> a

instance C Int where
  type T Int = Char

newtype WrappedInt = WrapInt Int deriving C

Then, if I understand the above proposal, the following code would be generated:

instance C WrappedInt where
  type T WrappedInt = T Int

which would violate injectivity.

comment:10 Changed 4 years ago by goldfire

Milestone: 8.0.18.2.1

Yes, as well it should. Derived instances are still type-checked, so this would be caught with no special-casing. I could imagine that the error message would be hard to understand, but that's the worst that would happen.

But this isn't going to happen by the 8.0 feature freeze, I'm afraid.

comment:11 Changed 4 years ago by thomie

Keywords: TypeFamilies added

comment:12 Changed 3 years ago by RyanGlScott

Cc: RyanGlScott added

comment:13 Changed 3 years ago by RyanGlScott

comment:14 Changed 3 years ago by RyanGlScott

Hm... what code would generated in this example?

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Kind

class C (a :: k) where
  type T k :: Type

instance C Int where
  type T Type = Int

--------------------

newtype MyInt = MyInt Int
  deriving C

comment:15 Changed 3 years ago by rwbarton

The definition of C should be illegal since it doesn't mention the variable a. Apparently that hasn't been fixed yet though, I thought it was?

comment:16 Changed 3 years ago by RyanGlScott

Why should C be illegal? The type parameters of T are a permutation of a proper subset of the class parameters (a and k), so it should be legal.

But moreover, I think the answer to my question in comment:14 is: you can't newtype-derive C for MyInt, as there's an associated type that doesn't mention the last type parameter of C. This is crucial, because if this doesn't hold, then we won't have a T instance to fall back on, making the whole derivation crumble. We'd just need to check for this condition beforehand.

comment:17 Changed 3 years ago by rwbarton

Oh that is a strange condition, but okay. (Maybe what I was thinking about was a new sanity condition on associated type instances, not their declarations.)

comment:18 Changed 3 years ago by simonpj

The recipe gave in comment:4 doesn't work for the example in comment:14. I could elaborate the recipe a bit thus:

class C x y z where
  type T y z x
  op :: x -> [y] -> z

newtype N a = MkN <rep-type> deriving( C )

-- Here the deriving clause would generate

instance C x y <rep-type> => C x y (N a) where
  type T y (N a) x = T y <rep-type> x
  op = coerce (op :: x -> [y] -> <rep-type>)

The recipe for generating the type instance is to replace the occurrence of z (which must occur) with <rep-type> on the LHS and RHS. I don't think it need be the last parameter of T, as the example shows.

I'm far from sure if this is really worth the effort of explaining and implementing it.

comment:19 Changed 3 years ago by RyanGlScott

Owner: changed from goldfire to RyanGlScott

Right, I didn't say the last type parameter of T had to be the newtype. Rather, the last type parameter of the class C (z in the example in comment:18) just has to occur somewhere in the type parameters of T.

I'm far from sure if this is really worth the effort of explaining and implementing it.

I disagree! Really, this is a quite straightforward idea (with a couple of small gotchas, like the one you observed), and I've implemented most of it already—I just need to polish up the documentation, update the GHC wiki, and post a Phabricator Diff.

comment:20 Changed 3 years ago by goldfire

Just to be clear on the design here: we plan on rejecting the code in comment:14, right? That is, for GND to work with associated types, the last parameter of the class must be mentioned in the associated type LHS. Then I'm on board.

comment:21 in reply to:  20 Changed 3 years ago by RyanGlScott

Replying to goldfire:

Just to be clear on the design here: we plan on rejecting the code in comment:14, right? That is, for GND to work with associated types, the last parameter of the class must be mentioned in the associated type LHS. Then I'm on board.

Yes, precisely. I'll make sure to mention this fact in the users' guide.

comment:22 Changed 3 years ago by RyanGlScott

Differential Rev(s): Phab:D2636
Status: newpatch

comment:23 Changed 3 years ago by Ryan Scott <ryan.gl.scott@…>

In 630d8817/ghc:

Allow GeneralizedNewtypeDeriving for classes with associated type families

Summary:
This implements the ability to derive associated type family instances
for newtypes automatically using `GeneralizedNewtypeDeriving`. Refer to the
users' guide additions for how this works; I essentially follow the pattern
laid out in https://ghc.haskell.org/trac/ghc/ticket/8165#comment:18.

Fixes #2721 and #8165.

Test Plan: ./validate

Reviewers: simonpj, goldfire, austin, bgamari

Reviewed By: simonpj

Subscribers: mpickering, thomie

Differential Revision: https://phabricator.haskell.org/D2636

GHC Trac Issues: #2721, #8165

comment:24 Changed 3 years ago by RyanGlScott

Resolution: fixed
Status: patchclosed
Test Case: deriving/should_compile/T8165, deriving/should_fail/T8165_fail1, deriving/should_fail/T8165_fail2

comment:25 Changed 18 months ago by RyanGlScott

Keywords: deriving added
Note: See TracTickets for help on using tickets.