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
comment:2 Changed 4 years ago by
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
One motivation for this is that it would finally provide us a way for users to "un-fundep" an argument without code repetition.
comment:5 Changed 4 years ago by
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
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.
comment:7 Changed 4 years ago by
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
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 follow-up: 11 Changed 4 years ago by
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
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 Changed 4 years ago by
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
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
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
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 follow-up: 17 Changed 4 years ago by
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
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 Changed 4 years ago by
=
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 supportGeneralizedNewtypeDeriving
.This also arises as a common idiom with the
mtl
, because you can use GND to deriveMonadState 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
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
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
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:22 Changed 4 years ago by
comment:23 Changed 4 years ago by
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
Cc: | adamgundry added |
---|
comment:25 Changed 4 years ago by
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
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 follow-up: 29 Changed 3 years ago by
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
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 follow-ups: 30 31 Changed 3 years ago by
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 follow-up: 33 Changed 3 years ago by
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 Changed 3 years ago by
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
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.)
comment:33 Changed 9 months ago by
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
I'm doubtful. Remember,
With that in mind, what would we make of
From a fundep point of view this is fine, provided
D
has a fundep. Expanding the default decl giveswhich makes no sense.