#11534: Allow class associated types to reference functional dependencies -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeFamilies, Resolution: | FunctionalDependencies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ekmett): Let's expand your example and see. {{{#!hs class C a b | a -> b where type Bar a type Bar a = b class D a b | a -> b instance D Int Bool instance D a b => C [a] [b] }}} If we have a functional dependency on `D` from `a -> b`, that secretly builds some type family for us, we use behind the scenes, right? Let's say that `D_ab` is the "hidden" type family implied by the functional dependency from `a -> b` then the expansion of {{{#!hs instance D a b => C [a] [b] }}} would be {{{#!hs instance D a b => C [a] [b] where type Bar [a] = [D_ab a] }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11534#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11534: Allow class associated types to reference functional dependencies -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeFamilies, Resolution: | FunctionalDependencies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ekmett): In smaller steps: {{{ type Bar [a] = C_ab [a] = [D_ab a] }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11534#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11534: Allow class associated types to reference functional dependencies -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeFamilies, Resolution: | FunctionalDependencies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ekmett): If I define {{{#!hs class Functor (c :: i -> i -> *) (d :: j -> j -> *) (f :: i -> j) | f -> c d }}} as opposed to {{{#!hs class Functor (f :: i -> j) where type Dom f :: i -> i -> * type Cod f :: j -> j -> * }}} then I go to define a subclass of `Functor`, I need to repeat `c` and `d`. {{{#!hs class Functor c d f => Faithful c d f | f -> c d }}} In some real world code I have this eventually swells to something like 8-9 parameters, which is clearly unwieldy. I can "lower" things back down, by using {{{#!hs class (c ~ Dom f, d ~ Cod f) => Functor (c :: i -> i -> *) (d :: j -> j -> *) (f :: i -> j) | f -> c d where type Dom f :: i -> i -> * type Cod f :: j -> j -> * fmap :: c a b -> d (f a) (f b) }}} and using something like {{{#!hs type Fun f = Functor (Dom f) (Cod f) f }}} as the superclass of {{{#!hs class Fun f => Faithful f where unfmap :: Cod f (f a -> f b) -> Dom f a b }}} at the cost of repeating myself between the fundep determined argument and the class associated type in every instance. {{{#!hs instance Functor (->) (->) ((->) e) where type Dom ((->) e) = (->) type Cod ((->) e) = (->) fmap = (.) }}} In the example from #11523, I have {{{#!hs instance (Category p, Category q) => Category (Nat p q) where type Ob (Nat p q) = Functor p q }}} Note: I can't run the trick the other way and put a type synonym there, since I can't partially apply it. which requires me to use functional dependencies for the definition of Functor or to be able to use the existing class/instance synonym trick mentioned there, which #11523 notes currently sends the compiler into a spin with `UndecidableSuperClasses` turned on. With the machinery I was seeking here, we'd be able to write just {{{#!hs instance Functor (->) (->) ((->) e) where fmap = (.) }}} but as you note this would require upgrading functional dependencies. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11534#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11534: Allow class associated types to reference functional dependencies -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeFamilies, Resolution: | FunctionalDependencies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ekmett): Then I get stuck when I get to the {{{#!hs instance (Category p, Category q) => Category (Nat p q) where type Ob (Nat p q) = Functor p q }}} line mentioned. I can't define {{{#!hs type Fun c d f = Functor (Dom f) (Cod f) f }}} and then put that in {{{#!hs instance (Category p, Category q) => Category (Nat p q) where type Ob (Nat p q) = Fun p q }}} because that involves partially applying a type family. For other reasons, I can't eta expand `Ob` to make it a type family with two parameters. Normally I'd do precisely what you suggest {{{#!hs class Functor (f :: i -> j) where type Dom f :: i -> i -> * type Cod f :: j -> j -> * }}} and then use the class/instance trick {{{#!hs class (Functor f, Dom f ~ c, Cod f ~ d) => FunctorOf c d f | f -> c d instance (Functor f, Dom f ~ c, Cod f ~ d) => FunctorOf c d f }}} to get a type family I can partially apply: {{{#!hs instance (Category p, Category q) => Category (Nat p q) where type Ob (Nat p q) = FunctorOf p q }}} but I get stuck due to #11523 causing the compiler to loop. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11534#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11534: Allow class associated types to reference functional dependencies -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeFamilies, Resolution: | FunctionalDependencies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):

I can't define {{{ type Fun c d f = Functor (Dom f) (Cod f) f }}} No indeed. So don't. Just have a single-parameter `Functor` class! {{{ class Functor (f :: i -> j) where type Dom f :: i -> i -> * type Cod f :: j -> j -> * }}} Now, I understand you are saying "a single-parameter `Functor` class is exactly what I would like but there is a problem". So rather than fix difficulties with the workaround, let's fix the actual problem. What exactly is it? What type family do you need to partially apply? So far we have `Dom` and `Cod`. Do you need to partially apply those? Can you just walk me through slowly the exact problem with the direct approach?

-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11534#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11534: Allow class associated types to reference functional dependencies -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeFamilies, Resolution: | FunctionalDependencies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ekmett):

What type family do you need to partially apply?

Given the single parameter `Functor` class, I would need to be able to supply something with kind `(i -> j) -> Constraint`, that says that its type argument is not just a Functor, but has a given `Dom` and a given `Cod`. {{{#!hs class (Functor f, Dom f ~ c, Cod f ~ d) => FunctorOf c d f | f -> c d instance (Functor f, Dom f ~ c, Cod f ~ d) => FunctorOf c d f }}} acts just like the type synonym {{{#!hs type FunctorOf c d f = (Functor f, Dom f ~ c, Cod f ~ d) }}} ''except'' it can be partially applied to the first two arguments to fix the Dom and Cod of its argument, whereas the type synonym version can't must be supplied all three arguments. Now I can answer

What type family do you need to partially apply?

The answer is `FunctorOf c d`. This lets me write the line {{{#!hs instance (Category p, Category q) => Category (Nat p q) where type Ob (Nat p q) = FunctorOf p q }}} Because I can "partially apply" FunctorOf p q to get something of kind `(i -> j) -> Constraint`. Unfortunately, as noted with #11523 with `UndecidableSuperClasses` turned on, I spin forever trying to use the `FunctorOf` definition in this place. The "obvious" fix then is to go through and replace the class associated type `Ob f :: i -> Constraint` with `type Ob f a :: Constraint`, but take an extra argument fails because I ultimately wind up needing to claim that `Ob (Nat p q)` is a functor from `p` to the category of constraints and it can't be if it can't be partially applied in its own right. Similar issues arise forcing the class/instance trick to deal with constraints elsewhere: {{{#!hs class (p, q) => p & q instance (p, q) => p & q }}} let's me talk about `(&) :: Constraint -> Constraint -> Constraint` or `(&) (Eq a) :: Constraint -> Constraint)`, whereas only a fully applied pair at the type level can be spoken of due to the limitations of the syntactic / semantic hack that we have in place for products of constraints.

Can you give concrete examples?

Every single definition in the `monads-tf` library has a significantly more verbose type signature than the ones in the `mtl`. {{{#!hs modify :: MonadState s m => (s -> s) -> m () tell :: MonadWriter e m => e -> m () ask :: MonadReader e m => m e local :: MonadReader e m => (e -> e) -> m a -> m a }}} vs. {{{#!hs modify :: MonadState m => (StateType m -> StateType m) -> m () tell :: MonadWriter m => WriterType m -> m () ask :: MonadReader m => m (EnvType m) local :: MonadReader m => (EnvType m -> EnvType m) -> m a -> m a }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11534#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11534: Allow class associated types to reference functional dependencies -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeFamilies, Resolution: | FunctionalDependencies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ekmett): Thanks! That will definitely get me unstuck for now, though I confess I'd still like a way to do something like this eventually. It'd go a long way towards ensuring that functional dependencies don't bit rot and cement them as more or less just a syntactic choice, rather than something radically different under the hood. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11534#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11534: Allow class associated types to reference functional dependencies -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeFamilies, Resolution: | FunctionalDependencies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by rwbarton): Another point is that GHC isn't very good at actually enforcing functional dependencies. For one thing, you can certainly fool it by putting orphan instances in different modules. But historically there have been several bugs where GHC failed to check the necessary conditions for the dependency to be functional under some cases. Notably, see #8634 and related tickets. For better or worse, after 7.8 fixed an often-abused bug, many users clamored for the old behavior. But that never quite happened, and the requests seem to have died out. In the past we've been fairly lackadaisical about such bugs since they don't seem to threaten type safety. From `class C a b | a -> b` and `C a b` and `C a b'` you cannot deduce `b ~ b'`. (In fact I think functional dependencies are much older than System FC.) But if we give access to the "functionally determined type" through a type family, then type safety is at stake so we have to treat such bugs seriously. Most likely, the implementation will force us to check the functional dependency correctly, and I would guess we will find a lot more programs that are currently abusing functional dependencies, to no real harm, and have to break them. Something to consider. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11534#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11534: Allow class associated types to reference functional dependencies -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeFamilies, Resolution: | FunctionalDependencies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ekmett): Consider the rather similar definitions of A and B below: {{{#!hs {-# language FunctionalDependencies, TypeFamilies, MultiParamTypeClasses, GeneralizedNewtypeDeriving #-} class A s m | m -> s instance A () Int class B m where type S m :: * instance B Int where type S Int = () }}} Now, {{{#!hs newtype X = X Int deriving (A ()) }}} works, but {{{#!hs newtype X = X Int deriving (B) }}} complains {{{ • Can't make a derived instance of ‘B X’ (even with cunning GeneralizedNewtypeDeriving): the class has associated types • In the newtype declaration for ‘X’ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11534#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11534: Allow class associated types to reference functional dependencies -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeFamilies, Resolution: | FunctionalDependencies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Interesting. I suppose you could say {{{ type family S m :: * class B m where {} type instance S Int = () instance B Int }}} Now you can say {{{ type instance S X = () newtype X = X Int deriving( B ) }}} This supplies the extra information nominally, whereas the fundep notation supplies it positionally. It might be advantageous to be able to give an associated type instance outside of a class instance decl. Thanks for the example. The problem is notational rather than fundamental; but still I can see it's annoying. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11534#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11534: Allow class associated types to reference functional dependencies -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeFamilies, Resolution: | FunctionalDependencies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Ah yes, #8165 indeed; provided that the rule in comment:7 there is indeed what is wanted in the cases that Edward describes. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11534#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11534: Allow class associated types to reference functional dependencies -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeFamilies, Resolution: | FunctionalDependencies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11534#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11534: Allow class associated types to reference functional dependencies -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeFamilies, Resolution: | FunctionalDependencies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ekmett): Using the rough elaboration scheme I mentioned above, isn't it just this? {{{#!hs instance Foo a b => Foo [a] [b] where type Foo_FD1 [a] = [Foo_FD1 a] }}} After all: {{{#!hs type Foo_FD1 [a] = [b] = [Foo_FD1 a] }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11534#comment:26 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11534: Allow class associated types to reference functional dependencies -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeFamilies, Resolution: | FunctionalDependencies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Addendum to the magic name idea: the ordering of fundeps would be irrelevant. So {{{#!hs class Bar a b c | a b -> c }}} and {{{#!hs class Bar a b c | b a -> c }}} would both generate a family named `Bar__1_2_DET_3#`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11534#comment:28 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11534: Allow class associated types to reference functional dependencies -------------------------------------+------------------------------------- Reporter: ekmett | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeFamilies, Resolution: | FunctionalDependencies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): I feel your pain. I think the choice to reuse `->` was a bit fishy from the start. I'd have no objection to using some symbol other than `::` if you'd prefer. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11534#comment:30 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11534: Allow class associated types to reference functional dependencies -------------------------------------+------------------------------------- Reporter: ekmett | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: TypeFamilies, Resolution: | FunctionalDependencies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Other | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to Simon:

This would make it possible for given constraints involving fundeps to work properly, which they don't at present (as ​Iavor points out).

Iavor is mostly complaining that currently you can declare instances that break FunDeps Consistency. (And because GHC knows that, it is conservative in applying type improvement via FunDeps. Also his examples either break the FunDeps Coverage Condition -- so needing `UndecidableInstances`; or use dependents (rhs of FunDeps arrow) with no free vars, so there's no algorithmic determinism.) If we desugar FunDeps to Type Families, and allow them to be Closed Type Families, then we can carry on breaking FunDeps Consistency, via overlapping equations. If OTOH we desugar FunDeps to Open Type Families, then we can't write overlapping equations; therefore we can't define (for example) a type- level Type Equality test. (This is somewhat orthogonal to whether we can write overlapping instances for the Class.) I can see the combination of FunDeps and `OverlappingInstances` is deadly for consistency. (To be precise, overlap of the determinants for FunDeps, on lhs of the arrow.) I can also see how terrifically useful it is -- for example for all sorts of record-like systems from HList onwards. I think I could make an argument that actually the combo FunDeps+Overlapping is consistent. That would need going back to the database Relational Theory from which Mark Jones borrowed FunDeps. And would require some discipline in what instances you declare. (I think most people actually observe that discipline, but GHC doesn't enforce it. I have an idea how we could help GHC enforce it -- a very old, recycled idea from Tom Schrijvers/CHRs.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11534#comment:32 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler