hi all, I'm trying to get my head around functional dependencies
I've created a simplified version of MonadReader
that has no functional dependencies
class MyMonadReader r m where
ask :: m r
When creating instances like
instance Monad m => MyMonadReader Bool (ReaderT r m) where
ask = pure True
instance Monad m => MyMonadReader String (ReaderT r m) where
ask = pure "string"
I see it compiling (as expected) and if I change MyMonadReader
definition to use functional dependencies
class MyMonadReader r m | m -> r where
ask :: m r
The code (as expected) does not compile.
Functional dependencies conflict between instance declarations:
instance Monad m => MyMonadReader Bool (ReaderT r m)
-- Defined at src/Machinery/FunDep.hs:29:10
instance Monad m => MyMonadReader String (ReaderT r m)
-- Defined at src/Machinery/FunDep.hs:31:10
If my instances look following
instance Monad m => MyMonadReader r (ReaderT r m) where -- <---------- THIS ONE WAS ADDED
ask = ReaderT.ask
instance Monad m => MyMonadReader Bool (ReaderT r m) where
ask = pure True
I would expect the code also to not to compile. But it does. And I'm truly puzzled.
Can anyone help with that puzzle? Why it does not complain, with a definition like class MyMonadReader r m | m -> r where
there should be only one instance for ReaderT r m , right?
i-am-tom:kcsongor: 1 hour ago
Hahah, thanks for the nudge! Totally forgot
i-am-tom:kcsongor: 1 hour ago
the tl;dr is that the functional dependency mechanism is triggered at the call site, not the definition site. Specifically, with a -> b, b will be inferred given an a that is concrete enough that it matches one instance
i-am-tom:kcsongor: 1 hour ago
if it isn't concrete enough to match one instance, you'll get an error (overlapping instances or ambiguous types, typically)
i-am-tom:kcsongor: 1 hour ago
The thing that makes this confusing is that GHC has some very basic checks that are run when you create instances with a fundep
i-am-tom:kcsongor: 1 hour ago
namely, if I have instance D a and instance D b, where a is a valid value for b (i.e. a is "more concrete"), GHC can tell you immediately that there's a problem
i-am-tom:kcsongor: 1 hour ago
If we have a case like yours:
instance Monad m => MonadReader Bool (ReaderT r m) where
ask = pure True
instance Monad m => MonadReader String (ReaderT r m) where
ask = pure "string"
It can also detect that, concretely, the same m maps to different (concrete!) r values
i-am-tom:kcsongor: 1 hour ago
So, why does your MonadReader r (ReaderT r m) not trigger this error?
i-am-tom:kcsongor: 1 hour ago
Well, we have two instance heads: MonadReader r (ReaderT r m) and MonadReader String (ReaderT r m)
i-am-tom:kcsongor: 1 hour ago
the first involves an equality between two variables in the instance head (both of which we've called r) and the second has a concrete value for this variable
i-am-tom:kcsongor: 1 hour ago
this makes this situation just a little bit too complicated for the basic checks
i-am-tom:kcsongor: 1 hour ago
for one, you may never instantiate r to anything but String - if so, is the instance overlapping, or duplicated?
i-am-tom:kcsongor: 1 hour ago
Another way that might help to look at it is to say MonadReader r (ReaderT s m) - the first instance adds the constraint that r ~ s, the second adds that r ~ String. It's not necessarily obvious that one is "more concrete" than the other, so we don't catch it in the basic check
i-am-tom:kcsongor: 1 hour ago
so yeah, the red herring is that you ever get an error when you define the class instances, because this isn't where the check occurs. It's just that GHC has some basic rules to catch common mistakes
i-am-tom:kcsongor: 1 hour ago
and is, in general, quite conservative with those rules. It doesn't error on instances unless it's sure they'd clash, just the same as it doesn't allow instances unless it's sure they're decidable (unless you turn the relevant extension on)