Opened 4 years ago

Last modified 9 months ago

#11534 new feature request

Allow class associated types to reference functional dependencies

Reported by: ekmett Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.10.3
Keywords: TypeFamilies, FunctionalDependencies Cc: adamgundry
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Other Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Consider:

class Foo i j | i -> j where
   type Bar i :: *
   type Bar i = j

This is rejected as j is not an argument to Bar, but when we realize any instance j will be a known type, determined by i, as told to us by the | i -> j functional dependency on the class.

This would likely require some sort of extra pass over the instances with class associated types of this form to elaborate them, or a slight modification of the default signature implementation for class associated types.

Change History (33)

comment:1 Changed 4 years ago by simonpj

I'm doubtful. Remember,

  • An associated type declaration is just convenient notation for a top-level declaration
  • Those default declarations are just an abbreviation for writing it out at every insttance

With that in mind, what would we make of

instance D a b => C [a] [b] where {}

From a fundep point of view this is fine, provided D has a fundep. Expanding the default decl gives

instance D a b => C [a] [b] where
  type Bar [a] = [b]

which makes no sense.

comment:2 Changed 4 years ago by ekmett

Let's expand your example and see.

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

instance D a b => C [a] [b]

would be

instance D a b => C [a] [b] where
  type Bar [a] = [D_ab a]

comment:3 Changed 4 years ago by ekmett

One motivation for this is that it would finally provide us a way for users to "un-fundep" an argument without code repetition.

comment:4 Changed 4 years ago by ekmett

In smaller steps:

type Bar [a] = C_ab [a] = [D_ab a]
Last edited 4 years ago by ekmett (previous) (diff)

comment:5 Changed 4 years ago by simonpj

No, there is no secret type function behind the scenes. Functional dependencies ONLY cause extra unification to take place.

One could imagine something more ambitious but it is not designed or implemented.

What repetition?

comment:6 Changed 4 years ago by ekmett

If I define

class Functor (c :: i -> i -> *) (d :: j -> j -> *) (f :: i -> j) | f -> c d

as opposed to

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.

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

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

type Fun f = Functor (Dom f) (Cod f) f

as the superclass of

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.

instance Functor (->) (->) ((->) e) where
  type Dom ((->) e) = (->)
  type Cod ((->) e) = (->)
  fmap = (.)

In the example from #11523, I have

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. This 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.

(I also can't eta expand the Ob type family to take another argument without causing issues with naturality later.)

With the machinery I was seeking here, we'd be able to write just

instance Functor (->) (->) ((->) e) where
  fmap = (.)

but as you note this would require upgrading functional dependencies.

Last edited 4 years ago by ekmett (previous) (diff)

comment:7 Changed 4 years ago by simonpj

You start by saying "If I define ... as opposed to ...".

But why to that? Why not use the "as opposed to" definition:

class Functor (f :: i -> j) where
  type Dom f :: i -> i -> *
  type Cod f :: j -> j -> *

Fewer parameters, no fundep, easy!

comment:8 Changed 4 years ago by ekmett

Then I get stuck when I get to the

instance (Category p, Category q) => Category (Nat p q) where
  type Ob (Nat p q) = Functor p q

line mentioned.

I can't define

type Fun c d f = Functor (Dom f) (Cod f) f

and then put that in

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

class Functor (f :: i -> j) where
  type Dom f :: i -> i -> *
  type Cod f :: j -> j -> *

and then use the class/instance trick

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:

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.

comment:9 Changed 4 years ago by ekmett

But there are other examples where this would be useful. e.g. mtl uses functional dependencies rather than type families, because the fundep versions of the type signatures are always less verbose, and users roundly rejected the monads-tf approach, but this results in a similar trap.

comment:10 Changed 4 years ago 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?

comment:11 in reply to:  9 Changed 4 years ago by simonpj

Replying to ekmett:

But there are other examples where this would be useful. e.g. mtl uses functional dependencies rather than type families, because the fundep versions of the type signatures are always less verbose

Can you give concrete examples?

comment:12 Changed 4 years ago 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.

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

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

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:

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.

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.

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

comment:13 Changed 4 years ago by simonpj

Very interesting. But the short term fix is to fix the original problem, with #11523, which I've now done (patch coming). SO that may unglue you.

comment:14 Changed 4 years ago 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.

comment:15 Changed 4 years ago by ekmett

Just another data point about when people use functional dependencies over class associated types:

I'm at the Compose conference in New York talking to Brian Hurt who is refactoring the monad-control package to switch to functional dependencies from a class associated type so that he can support GeneralizedNewtypeDeriving.

This also arises as a common idiom with the mtl, because you can use GND to derive MonadState MyState.

comment:16 Changed 4 years ago 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.

comment:17 in reply to:  15 Changed 4 years ago by simonpj

=

I'm at the Compose conference in New York talking to Brian Hurt who is refactoring the monad-control package to switch to functional dependencies from a class associated type so that he can support GeneralizedNewtypeDeriving.

This also arises as a common idiom with the mtl, because you can use GND to derive MonadState MyState.

Would you (or he) care to give a small self-contained example of why GND works for fundeps but not for associated types?

comment:18 Changed 4 years ago by ekmett

Consider the rather similar definitions of A and B below:

{-# 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,

newtype X = X Int deriving (A ())

works, but

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’

comment:19 Changed 4 years ago by ekmett

A related common idiom you can spot in the wild using the mtl is to do something like

newtype M a = M (ReaderT MyEnv (StateT MyState (WriterT MyLog IO)) a)
  deriving (Functor, Applicative, Monad, MonadIO, MonadReader MyEnv, MonadState MyState, MonadWriter MyLog, MonadIO)

resulting in a custom monad where you can filter out as many of the instances as you don't like in 2 lines rather than in hand-rolling one in 60.

E.g. haskeline's InputT is more or less an example of this, although Judah explicitly hides the MonadReader instance.

comment:20 Changed 4 years ago 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.

comment:21 Changed 4 years ago by rwbarton

See #8165.

comment:22 Changed 4 years ago 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.

comment:23 Changed 4 years ago by adamgundry

Going back to imagining something more ambitious to tackle the original issue, how feasible would it be to take a class

class Foo i j | i -> j

instance Foo Int Bool

and elaborate it into something like

class j ~ Foo_FD1 i => Foo i j where
  type Foo_FD1 i :: *

instance Foo Int Bool where
  type Foo_FD1 Int = Bool

so that functional dependencies really would build a type family behind the scenes, and the class would carry explicit evidence? This would make it possible for given constraints involving fundeps to work properly, which they don't at present (as Iavor points out).

Of course, we'd need to figure out how the user should be allowed to refer to such type families, and how the constraint solver should treat them. Moreover, this translation might break programs that are abusing fundeps (comment:16). But perhaps it would be worth exploring.

comment:24 Changed 4 years ago by adamgundry

Cc: adamgundry added

comment:25 Changed 4 years ago by simonpj

Yes I've often thought of doing this. An alternative, which no one has ever fleshed out, would be to extend System FC somehow to provide evidence for functional dependencies. But what Adam suggests here is more or less precisely that; the Foo class is a record that has (j ~ Foo_FD1 i) as one of its fields; that is, evidence that (j ~ Foo_FD1 i).

I worry a bit about how elaborate the translation might be, and whether error messages might mention these strange functions.

An alternative is just to use the type-family approach in the first place.

Hmm. Maybe we could use default declarations to make it even easier:

class j ~ Foo_FD1 i => Foo i j where
  type Foo_FD1 i :: *
  type Foo_FD1 i = j

instance Foo Int Bool where
  -- Nothing

This is currently rejected because j is not bound on the LHS of the default decl, but if we allowed it, then we'd get, well, precisely what we want.

Oh, the idea doesn't work at all. Consider

instance Foo a b => Foo [a] [b] where
  type Foo_FD1 [a] = [F a]  -- This RHS is not so easy to generate!

comment:26 Changed 4 years ago by ekmett

Using the rough elaboration scheme I mentioned above, isn't it just this?

instance Foo a b => Foo [a] [b] where
    type Foo_FD1 [a] = [Foo_FD1 a]

After all:

type Foo_FD1 [a] = [b] = [Foo_FD1 a]

comment:27 Changed 3 years ago by dfeuer

If people want to go forward with desugaring fundeps to type families (sounds great to me), I think it would be lovely to add naming syntax:

class Foo a b c d | (Q, R :: a -> b c), (S :: b d -> a)

would desugar to

class (b ~ Q a, c ~ R a, a ~ S b d) => Foo a b c d where
  type family Q a
  type family R a
  type family S b d

To work with classes that lack named fundeps, some nasty names could be made available.

class Foo a b c d | a -> b c, b d -> a

could desugar to use type families with (exposed, but unlikely) names like Foo__1_DET_2#, Foo__1_DET_3#, and Foo__2_4_DET_1#, naming the positions that determine other positions.

It might be good to add dysfunctional "soft dependencies" at the same time, with ~> syntax and vague semantics to be pinned down later (the idea being that soft dependencies would only guide inference, as best they could, without being relied upon for type checking).

comment:28 Changed 3 years ago by dfeuer

Addendum to the magic name idea: the ordering of fundeps would be irrelevant. So

class Bar a b c | a b -> c

and

class Bar a b c | b a -> c

would both generate a family named Bar__1_2_DET_3#.

comment:29 in reply to:  27 ; Changed 3 years ago by goldfire

Replying to dfeuer:

If people want to go forward with desugaring fundeps to type families (sounds great to me), I think it would be lovely to add naming syntax:

class Foo a b c d | (Q, R :: a -> b c), (S :: b d -> a)

I tend to like the option to give names, but I cringe at this syntax. The :: in there activates my brain's type parser. Then, that parser successfully processes a -> b c. But then my brain experiences quite a jarring type error when it tries to treat the result of that parse as a functional dependency.

I have no better suggestion here, and I would probably admit that this is the best available syntax. I just hate experiencing type errors in my brain just as much as in my running programs! Haskell generally prevents the latter. I have no good idea how to prevent the former, in general.

comment:30 in reply to:  29 ; Changed 3 years ago 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.

comment:31 in reply to:  29 Changed 3 years ago by dfeuer

Another thought: this might be more efficient if dependencies that determine multiple types could be represented by a single type family. However, I know nothing about type checking efficiency matters.

comment:32 Changed 2 years ago by AntC

Replying to Adam comment:23:ticket:11534 :

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 Sulzman&Stuckey/CHRs.)

Last edited 2 years ago by AntC (previous) (diff)

comment:33 in reply to:  30 Changed 9 months ago by AntC

Replying to dfeuer:

I think the choice to reuse -> was a bit fishy from the start.

The arrow was borrowed straight from database Functional Dependencies. (I guess it helped that -> was already a recognised lexeme.)

But note that Mark Jones' original proposal was that FunDeps should look like this

class Foo a b c d  | {a} -> {b, c}, {b, d} -> {a}  where ...

IOW: the determinant and dependent are sets of parameters (order immaterial). That's exactly how they look in database theory. b d does indeed excite in my brain that is tyvar b applied to d. (The Haskell abbreviated form was also taken over into injective type families, where it gives a potential syntactic ambiguity.)

So the fishiness arose from dropping the set notation braces with commalist.

I'd have no objection to using some symbol other than :: if you'd prefer.

Aside from how to bind naming for a FunDep, beware that a Type Familiy's parameters are positional whereas a FunDep's are not. IOW this is (supposed to be) an entirely equivalent class decl

class Foo a b c d  | d b -> a, a -> b c
Note: See TracTickets for help on using tickets.