Opened 23 months ago

Closed 23 months ago

Last modified 22 months ago

#14661 closed feature request (wontfix)

Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.4.1-alpha1
Keywords: DerivingStrategies, deriving, TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This works fine

{-# Language PolyKinds #-}
{-# Language GADTs #-}
{-# Language GeneralizedNewtypeDeriving #-}
{-# Language InstanceSigs #-}
{-# Language RankNTypes #-}
{-# Language ScopedTypeVariables #-}
{-# Language StandaloneDeriving #-}
{-# Language TypeApplications #-}
{-# Language DataKinds #-}
{-# Language DerivingStrategies #-}
{-# Language TypeFamilies #-}

import Data.Kind
import Control.Category
import Prelude hiding (id, (.))
import Data.Coerce

data TY = TI | TB

type family
  Interp ty where
  Interp TI = Int
  Interp TB = Bool

newtype Ixed :: TY -> TY -> Type where
  Ixed :: (Interp ix -> Interp ix')
       -> (Ixed ix ix')
  -- deriving newtype Category

instance Category Ixed where
  id :: forall a. Ixed a a
  id = coerce (id @(->) @(Interp a))

  (.) :: forall b c a. Ixed b c -> Ixed a b -> Ixed a c
  (.) = coerce ((.) @(->) @(Interp b) @(Interp c) @(Interp a))

This instance can not be derived using newtype deriving. Commenting the Category-instance out and uncommenting deriving newtype Category results in an error

$ ghci2 -ignore-dot-ghci hs/164-trac.hs
GHCi, version 8.5.20180105: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( hs/164-trac.hs, interpreted )

hs/164-trac.hs:28:20: error:
    • Can't make a derived instance of
        ‘Category Ixed’ with the newtype strategy:
        cannot eta-reduce the representation type enough
    • In the newtype declaration for ‘Ixed’
   |
28 |   deriving newtype Category
   |                    ^^^^^^^^
Failed, no modules loaded.
Prelude> 

I may have asked this before, but can we make GHC smart enough to derive this instance? It consists entirely of the right visible type application of method: method = coerce (method @a @b @..)

Change History (15)

comment:1 Changed 23 months ago by simonpj

Interesting. The type family is a red herring. Same thing happens with data Interp a = I.

comment:2 in reply to:  1 Changed 23 months ago by RyanGlScott

Replying to simonpj:

Same thing happens with data Interp a = I.

Well sure—you can't use GeneralizedNewtypeDeriving on a non-newtype.

I agree that the type family is a red herring, though. Let's look at a slightly simpler example:

{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

import Control.Category

data Bar a

newtype Foo a b = MkFoo (Bar a -> Bar b)
  deriving newtype Category
    • Can't make a derived instance of
        ‘Category Foo’ with the newtype strategy:
        cannot eta-reduce the representation type enough
    • In the newtype declaration for ‘Foo’
  |
9 |   deriving newtype Category
  |                    ^^^^^^^^

Why is this happening? As per the specification of GeneralizedNewtypeDeriving in the users' guide, GHC must be able to eta-convert Foo's underlying representation type (i.e., Bar a -> Bar b) in order to generate a context. But you cannot eta-reduce the type variables a and b from Bar a -> Bar b, try as you might.


Returning to your original example, you claim that the instance you hand-wrote "consists entirely of the right visible type application of method: method = coerce (method @a @b @..)", but this isn't true. Look at your id implementation, for instance:

  id :: forall a. Ixed a a
  id = coerce (id @(->) @(Interp a))

This is a good deal more clever than what GeneralizedNewtypeDeriving currently does. GND would try to coerce from id :: forall a. Ixed a a to id :: forall a. ??? a a, where ??? is the eta-reduced representation type (that we were unable to obtain, as explained previously). But your implementation tunnels down through (->) and exploits the fact that Interp happens to be present on both sides of the arrow.

This insider knowledge would not be particularly simple to teach GHC—for instance, what happens if you chance Ixed to be of type (Interp ix -> Maybe (Interp ix') -> (Ixed ix ix')? Moreover, the kinds of tricks that would work for Category/(->) would likely not be applicable for other type class/type constructor combinations.

tl;dr I claim this is not a bug, but rather a misunderstanding of how GeneralizedNewtypeDeriving works.

comment:3 Changed 23 months ago by Iceland_jack

Type: bugfeature request

Changed it to a feature request. This is actually a new deriving strategy.

A second derivation for the same thing: I am able to mechanically write type constructors like this (clever / insider knowledge? I don't think so) and it compiles:

instance Category Ixed where
  id = Ixed id
  Ixed f . Ixed g = Ixed (f . g)

With this derivation your other example newtype Ixed ix ix' = Ixed (Interp ix -> Maybe (Interp ix')) does not compile.

I am experimenting with categories over type families / data types and the above instance is boilerplate. This space may be too limited to be worth it, maybe someone else has useful examples of a different character.

comment:4 Changed 23 months ago by Iceland_jack

Similar example from Conal's Compiling to Categories, 7.6 Incremental Computation

class HasDelta a where
  type Delta a :: Type

newtype DelX a b = DelX (Delta a -> Delta b)

instance Category DelX where
  type Ok DelX = HasDelta
  id = DelX id
  DelX g . DelX f = DelX (g . f)

instance Cartesian DelX where
  exl = DelX exl
  exr = DelX exr
  DelX f &&& DelX g = DelX (f &&& g)

comment:5 Changed 23 months ago by Iceland_jack

This can be derived (clunkily) with GND + singletons

import Data.Singletons

type Cat ob = ob -> ob -> Type

newtype WRAP :: (k' ~> k) -> (Cat k -> Cat k') where
  WRAP :: cat (f@@a) (f@@b) 
       -> WRAP f cat a b

instance Category cat => Category (WRAP f cat) where
  id :: forall a. WRAP f cat a a
  id = WRAP (id @cat @(f@@a))

  (.) :: forall b c a. WRAP f cat b c -> WRAP f cat a b -> WRAP f cat a c
  WRAP f . WRAP g = WRAP ((.) @cat @(f@@b) @(f@@c) @(f@@a) f g)

data InterpSym0 :: TY ~> Type
type instance InterpSym0 @@ ty = Interp ty

+

newtype Ixed a b = Ixed (WRAP InterpSym0 (->) a b)
  deriving newtype Category

or with -XDerivingVia

newtype Ixed a b = Ixed (Interp a -> Interp b)
  deriving Category
    via (WRAP InterpSym0 (->) a b)
Last edited 23 months ago by Iceland_jack (previous) (diff)

comment:6 Changed 23 months ago by RyanGlScott

My belief is that DerivingVia is exactly what you're looking for (instead of attempting to encode this into GHC somehow in an ad hoc fashion).

comment:7 Changed 23 months ago by Iceland_jack

Yes this logic should rather be defined in a module/library than in GHC. Any thoughts Simon? Can close this

comment:8 Changed 23 months ago by simonpj

Well sure—you can't use GeneralizedNewtypeDeriving on a non-newtype

The newtype is called Ixed. The type function is Interp. Turning it into a data type (and removing the instances) simplifies the example, but does not affect the payload.

comment:9 Changed 23 months ago by simonpj

Trac 14661

Hmm. What is DerivingVia? Is it implemented, documented?

I agree this is a feature request, going significantly beyond what GHC can do right now.

However, the new feature looks tantalisingly close. E.g. for instance Category Ixed we need to find

  id :: forall a. Ixed a a

Expanding the type representation gives

  id1 :: forall a. Interp a -> Interp a

We have in hand the (->) instance of Category:

  id @(->) :: forall b. b -> b

and in fact we can readily instantiate id @(->)@ to match the needed type.

So, could we imagine this? Given

newtype N a b = MkN (R t1 t2 t3) deriving( Category )

we want to derive instance ... => C N given instance ... => C R. Suppose we have a method in class C

class R (c :: * -> * -> *) where
   foo :: forall p q. ...(c s1 s2)...

(NB: for now I will assume that c appears fully applied in foo's type.) Then we will have available foo1 :: forall p q. ...(R s1 s2)... and we want to get foo2 :: forall p q. ...(N s1 s2)....

Well from the newtype declaration we have an axiom that equates the representation types of (N a b) and (R t1 t2 t3):

ax :: forall a b.  N a b  ~R  R t1 t2 t3

So, if we could find

  foo3 :: forall p q. ...(R t1[s1/a,s2/q]
                            t2[s1/a,s2/q]
                            t3[s1/a,s2/q]) ...

we'd be home and dry, because then we can use ax to get from foo3 to foo2.

How can we get foo3? Well, it's possible that we can get it just by instantiating the type of foo1. In the case of id in Category we have

id1 :: forall a. (->) a a   -- Available, given
id2 :: forall a. Ixed a a   -- Wanted
id3 :: forall a. (->) (Interp a) (Interp a)   -- Wanted

And indeed we can get id3 from id1 by instantiation.

This won't always work as Ryan points out, but sometimes. And I suppose we could work that out.

It seems rather elaborate though!

comment:10 Changed 23 months ago by RyanGlScott

Resolution: wontfix
Status: newclosed

Apologies simonpj, comment:6 wouldn't have made sense except to Iceland_jack, myself, and a handful of other people.

DerivingVia is the code name we're using to describe a work-in-progress deriving strategy that we're developing, based on this HaskellX talk that Iceland_jack gave. This would allow you to write something of the form:

newtype Ixed a b = Ixed (Interp a -> Interp b)
  deriving Category
    via (WRAP InterpSym0 (->) a b)

Where WRAP is a separate data type that has exactly the right Category instance that you'd want for Ixed. It would generate the following code:

instance Category Ixed where
  id  = coerce @(forall a. Ixed a a) @(forall a. WRAP InterpSym0 (->) a a) id
  (.) = coerce @(forall a b c. Ixed b c -> Ixed a b -> Ixed a c) @(forall a b c. WRAP InterpSym0 (->) b c -> WRAP InterpSym0 (->) a b -> WRAP InterpSym0 (->) a c) (.)

Another way of thinking about it is that it's an even more generalized form of GeneralizedNewtypeDeriving where the user is allowed to specify their own type to coerce from (instead of being required to use a newtype's underlying representation type).

It's not fully documented at the moment, but we do have a WIP specification here if you're curious.

Anyways, I'll opt to close this, since Iceland_jack seems OK with the idea of using DerivingVia to accomplish this task.

comment:11 in reply to:  9 Changed 22 months ago by Iceland_jack

Replying to simonpj:

However, the new feature looks tantalisingly close.

This won't always work as Ryan points out, but sometimes. And I suppose we could work that out.

It seems rather elaborate though!

I agree that it's tantalising, if you think it's a general enough solution, enough “bang for the buck” then re-open. But there is no hurry on my end, I'd like more examples that need this.

comment:12 Changed 22 months ago by Iceland_jack

I don't know if this should be a separate ticket but it is another case that can be derived only by expanding constructors

import Data.Monoid (Endo)

newtype ENDO = ENDO (forall xx. Endo xx)

instance Semigroup ENDO where
  ENDO f <> ENDO g = ENDO (f <> g)

instance Monoid ENDO where
  mempty = ENDO mempty

Can also be derived using via and quantified constraints (or constraints)

newtype ENDO = ENDO (forall xx. Endo xx)
  deriving (Semigroup, Monoid)
    via (Forall Endo)

----

instance Forall :: (k -> Type) -> Type where
  Forall :: (forall xx. f xx) -> Forall f

instance (forall xx. Semigroup (f xx)) => Semigroup (Forall f) where
  Forall xs <> Forall ys = Forall (xs <> ys)

instance (forall xx. Monoid (f xx)) => Monoid (Forall f) where
  mempty = Forall mempty
Last edited 22 months ago by Iceland_jack (previous) (diff)

comment:13 Changed 22 months ago by Iceland_jack

Here is an interesting one:

class ListLike f where
  nil  :: f a
  cons :: a -> f a -> f a
  (·)  :: f a -> f a -> f a

newtype LL a = LL (forall zz. ListLike zz => zz a)

You can implement (but not derive) ListLike LL:

instance ListLike LL where
  nil :: LL a
  nil = LL nil
  
  cons :: a -> LL a -> LL a
  cons a (LL as) = LL (cons a as)
  
  (·) :: LL a -> LL a -> LL a
  LL as · LL bs = LL (as · bs)

I'll add further examples to this gist.

comment:14 Changed 22 months ago by RyanGlScott

Your example in comment:12 is quite interesting. It only fails because GHC attempts to generate the constraint Semigroup (forall xx. Endo xx) and immediately chokes. But we never intended to generate that constraint—we wanted forall xx. Semigroup (Endo xx), a quantified constraint!

I would posit that if we derive instances that require slapping a class onto a type, we should be pushing the class through foralls and other constraints. For instance, if we want to apply Semigroup to forall xx. Endo xx, we should push Semigroup through forall xx to obtain forall xx. Show (Endo xx), and then chuck that into the constraint solver.

(I think this same strategy would work with the program in comment:13, as we really want to generate the constraint forall zz. ListLike zz => ListLike zz, which could be discharged immediately. But that might require #14733 to be fixed, so perhaps it's not as good of a motivating example.)

All of this assumes QuantifiedConstraints, of course, so it's not really actionable right now. Iceland_jack, perhaps you could open a separate ticket for this? (With the keyword deriving in there so that I can find it later.)

comment:15 Changed 22 months ago by RyanGlScott

I had a burning curiosity, so I quickly implemented the ideas sketched out in comment:14 to see if they'd work. To my great surprise, the changes almost work perfectly! But I did use the word "almost"—there's a pretty big snag that prevents newtype ENDO = ENDO (forall xx. Endo xx) deriving Semigroup from working. To better explain what's going on, here is the code that -ddump-deriv is producing:

{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
module Bug where

import Data.Coerce
import Data.Kind
import Data.List.NonEmpty
import Data.Monoid
import Data.Semigroup

newtype ENDO = ENDO (forall a. Endo a)

instance Semigroup ENDO where
  (<>)
    = coerce
        @((forall (a_a3ZJ :: Type). Endo a_a3ZJ) -> (forall (a_a3ZJ :: Type). Endo a_a3ZJ) -> forall (a_a3ZJ :: Type). Endo a_a3ZJ)
        @(ENDO -> ENDO -> ENDO)
        (<>)
  sconcat
    = coerce
        @(NonEmpty (forall (a_a3ZJ :: Type). Endo a_a3ZJ) -> forall (a_a3ZJ :: Type). Endo a_a3ZJ)
        @(NonEmpty ENDO -> ENDO)
        sconcat
  stimes
    = coerce
        @(forall (b_a2d8 :: Type). Integral b_a2d8 => b_a2d8 -> (forall (a_a3ZJ :: Type). Endo a_a3ZJ) -> forall (a_a3ZJ :: Type). Endo a_a3ZJ)
        @(forall (b_a2d8 :: Type). Integral b_a2d8 => b_a2d8 -> ENDO -> ENDO)
        stimes

(<>) and stimes actually typecheck without issue, to my great joy. But alas, sconcat does not:

Bug.hs:25:9: error:
    • Couldn't match type ‘forall a_a3ZJ1. Endo a_a3ZJ1’
                     with ‘Endo a_a3ZJ’
      Expected type: NonEmpty (forall a_a3ZJ1. Endo a_a3ZJ1)
                     -> Endo a_a3ZJ
        Actual type: NonEmpty (Endo a_a3ZJ) -> Endo a_a3ZJ
    • In the third argument of ‘coerce’, namely ‘sconcat’
      In the expression:
        coerce
          @(NonEmpty (forall (a_a3ZJ :: Type). Endo a_a3ZJ)
            -> forall (a_a3ZJ :: Type). Endo a_a3ZJ)
          @(NonEmpty ENDO -> ENDO)
          sconcat
      In an equation for ‘sconcat’:
          sconcat
            = coerce
                @(NonEmpty (forall (a_a3ZJ :: Type). Endo a_a3ZJ)
                  -> forall (a_a3ZJ :: Type). Endo a_a3ZJ)
                @(NonEmpty ENDO -> ENDO)
                sconcat
   |
25 |         sconcat
   |         ^^^^^^^

It seems that GHC is unwilling to instantiate sconcat at an impredicative type, even with ImpredicativeTypes enabled. What's annoying is that this typechecks:

{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
module Bug2 where

import Data.Coerce
import Data.Monoid
import Data.List.NonEmpty
import Data.Semigroup

newtype ENDO = ENDO (forall a. Endo a)

test :: (NonEmpty (forall a. Endo a) -> (forall a. Endo a)) -> (NonEmpty ENDO -> ENDO)
test = coerce @(NonEmpty (forall a. Endo a) -> (forall a. Endo a)) @(NonEmpty ENDO -> ENDO)

But, as we saw in the earlier example, trying to give sconcat as an argument to a function with such a type signature would cause GHC to choke. It seems that we'd need more impredicative smarts to make this all work.

Note: See TracTickets for help on using tickets.