Functional dependencies?
johnsonwj opened this issue · 6 comments
Heyo! I apologize in advance that this may end up being silly because I confess that I am still pretty new to most GHC extensions, but I have been racking my brain over the language option docs in the GHC user guide and I can't seem to get anywhere.
TLDR: Is it possible to use functional dependencies in classes like State s m or Reader r m or is that not feasible in the design of this library?
I saw the announcement for this library on reddit and decided to try to use it to do stuff. Here's a basic example that fails to compile without AllowAmbiguousTypes:
{-# LANGUAGE AllowAmbiguousTypes #-}
module Foo where
import Control.Effect.State
import Control.Effect.Writer
import System.Random
addNum :: forall g m. (RandomGen g, State g m, Writer [Int] m) => m ()
addNum = do
gen <- get @g
let (num, gen') = randomR @Int @g (0, 100) gen
put gen'
tell [num]If I don't include the pragma, I get the following error:
src/Foo.hs:9:11: error:
• Could not deduce (RandomGen g0)
from the context: (RandomGen g, State g m, Writer [Int] m)
bound by the type signature for:
addNum :: forall g (m :: * -> *).
(RandomGen g, State g m, Writer [Int] m) =>
m ()
at src/Foo.hs:9:11-70
The type variable ‘g0’ is ambiguous
• In the ambiguity check for ‘addNum’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature:
addNum :: forall g m.
(RandomGen g, State g m, Writer [Int] m) => m ()
|
9 | addNum :: forall g m. (RandomGen g, State g m, Writer [Int] m) => m ()
|
which is presumably because GHC has no reason to believe that an arbitrary m () could possibly satisfy the constraints.
Moreover, even with that flag, I need to sprinkle around type applications; otherwise...
src/Foo.hs:11:12: error:
• Could not deduce (State s0 m) arising from a use of ‘get’
from the context: (RandomGen g, State g m, Writer [Int] m)
bound by the type signature for:
addNum :: forall g (m :: * -> *).
(RandomGen g, State g m, Writer [Int] m) =>
m ()
at src/Foo.hs:9:1-70
The type variable ‘s0’ is ambiguous
Relevant bindings include addNum :: m () (bound at src/Foo.hs:10:1)
These potential instances exist:
instance Monad m => State s (StateT s m)
-- Defined in ‘Control.Effect.State’
...plus one instance involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In a stmt of a 'do' block: gen <- get
In the expression:
do gen <- get
let (num, gen') = randomR ... gen
put gen'
tell [num]
In an equation for ‘addNum’:
addNum
= do gen <- get
let (num, gen') = ...
put gen'
....
|
11 | gen <- get
| ^^^
src/Foo.hs:12:23: error:
• Could not deduce (Random a0) arising from a use of ‘randomR’
from the context: (RandomGen g, State g m, Writer [Int] m)
bound by the type signature for:
addNum :: forall g (m :: * -> *).
(RandomGen g, State g m, Writer [Int] m) =>
m ()
at src/Foo.hs:9:1-70
The type variable ‘a0’ is ambiguous
Relevant bindings include num :: a0 (bound at src/Foo.hs:12:10)
These potential instances exist:
instance Random Integer -- Defined in ‘System.Random’
instance Random Bool -- Defined in ‘System.Random’
instance Random Char -- Defined in ‘System.Random’
...plus four others
...plus 29 instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the expression: randomR (0, 100) gen
In a pattern binding: (num, gen') = randomR (0, 100) gen
In the expression:
do gen <- get
let (num, gen') = randomR ... gen
put gen'
tell [num]
|
12 | let (num, gen') = randomR (0, 100) gen
| ^^^^^^^^^^^^^^^^^^^^
src/Foo.hs:12:32: error:
• Could not deduce (Num a0) arising from the literal ‘0’
from the context: (RandomGen g, State g m, Writer [Int] m)
bound by the type signature for:
addNum :: forall g (m :: * -> *).
(RandomGen g, State g m, Writer [Int] m) =>
m ()
at src/Foo.hs:9:1-70
The type variable ‘a0’ is ambiguous
Relevant bindings include num :: a0 (bound at src/Foo.hs:12:10)
These potential instances exist:
instance Num Integer -- Defined in ‘GHC.Num’
instance Num Double -- Defined in ‘GHC.Float’
instance Num Float -- Defined in ‘GHC.Float’
...plus two others
...plus 39 instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the expression: 0
In the first argument of ‘randomR’, namely ‘(0, 100)’
In the expression: randomR (0, 100) gen
|
12 | let (num, gen') = randomR (0, 100) gen
| ^
src/Foo.hs:14:5: error:
• Could not deduce (Writer [a0] m) arising from a use of ‘tell’
from the context: (RandomGen g, State g m, Writer [Int] m)
bound by the type signature for:
addNum :: forall g (m :: * -> *).
(RandomGen g, State g m, Writer [Int] m) =>
m ()
at src/Foo.hs:9:1-70
The type variable ‘a0’ is ambiguous
Relevant bindings include
num :: a0 (bound at src/Foo.hs:12:10)
addNum :: m () (bound at src/Foo.hs:10:1)
These potential instances exist:
two instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In a stmt of a 'do' block: tell [num]
In the expression:
do gen <- get
let (num, gen') = randomR ... gen
put gen'
tell [num]
In an equation for ‘addNum’:
addNum
= do gen <- get
let (num, gen') = ...
put gen'
....
|
14 | tell [num]
|
Here's the same thing in mtl; in particular, I no longer need AllowAmbiguousTypes, and I can even get away with leaving out the type applications:
import Control.Monad.State
import Control.Monad.Writer
import System.Random
addNum :: forall g m. (RandomGen g, MonadState g m, MonadWriter [Int] m) => m ()
addNum = do
gen <- get
let (num, gen') = randomR (0, 100) gen
put gen'
tell [num]Assuming that I'm just bad at type magic, I asked over at the Haskell discourse if anyone could spot what I was missing. artem's comment pointed me to a possible solution: namely that the State class in eff does not specify a functional dependency m -> s.
To my eye this would make sense; whatever monad we happen to be in should be able to fix the type of state that it's holding. But if I just naively try to add that dependency, eff no longer compiles; specifically, changing this line to class Monad m => State s m | m -> s where yields
src/Control/Effect/State.hs:40:10: error:
• Illegal instance declaration for ‘State s (EffT t m)’
The liberal coverage condition fails in class ‘State’
for functional dependency: ‘m -> s’
Reason: lhs type ‘EffT t m’ does not determine rhs type ‘s’
Un-determined variable: s
• In the instance declaration for ‘State s (EffT t m)’
|
40 | instance (Monad (t m), Send (State s) t m) => State s (EffT t m) where
|
Feeling around Internal.hs I also added | m -> eff here and here, and | m -> effs here. Now I get:
src/Control/Effect/Internal.hs:194:10: error:
• Illegal instance declaration for ‘Handle 'True eff t m’
The liberal coverage condition fails in class ‘Handle’
for functional dependency: ‘m -> eff’
Reason: lhs type ‘m’ does not determine rhs type ‘eff’
Un-determined variable: eff
• In the instance declaration for ‘Handle 'True eff t m’
|
194 | instance eff (t m) => Handle 'True eff t m where
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
src/Control/Effect/Internal.hs:198:10: error:
• Illegal instance declaration for ‘Handle 'False eff t m’
The liberal coverage condition fails in class ‘Handle’
for functional dependency: ‘m -> eff’
Reason: lhs type ‘m’ does not determine rhs type ‘eff’
Un-determined variable: eff
• In the instance declaration for ‘Handle 'False eff t m’
|
198 | instance (MonadTransControl t, eff m) => Handle 'False eff t m where
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
src/Control/Effect/Internal.hs:285:10: error:
• Illegal instance declaration for ‘Can effs m’
The liberal coverage condition fails in class ‘Can’
for functional dependency: ‘m -> effs’
Reason: lhs type ‘m’ does not determine rhs type ‘effs’
Un-determined variable: effs
• In the instance declaration for ‘Can effs m’
|
285 | instance All effs m => Can effs m
|
At this point I am thoroughly out of my league with type families; my guess is that the solution has to do with type family dependencies but I am not sure what that would look like. Based on comparing the examples in the doc to what I see here, there is too much going on that I don't yet get :(
If functional dependencies are simply not possible, is the use of AllowAmbiguousTypes for this sort of thing unavoidable? Or is there another option I am missing?
Thanks for any advice!!
I have been poking around the docs for type families - maybe associated type families will be enough to represent these constraints, e.g.
class Monad m => MonadState m where
data S m
get :: m (S m)
put :: S m -> m ()This would avoid "mixing flavors" with fundeps, since it seems that the same type-level logic can be represented in this way, and eff already makes effective (sorry) use of type families internally. I just need to tinker around more with Control.Effect.Internal - much of this is still new and mysterious for me, so unless it's obvious to anyone else whether or not that is even possible, I'll be seeing if that works!
After playing around some time with this library myself, I came to a similar conclusion: Functional dependencies break the automatic lifting machinery, and I think it is impossible to fix it in its current form.
As far as I understand it, the automatic lifting machinery works in a way that says: "Every transformer stack t m a can handle an effect, it is only the question if t m handles it or m handles it." This is not compatible with a functional dependency m -> s, i.e. you cannot convince the type system to infer s from a generic (see "every" above) transformer stack EffT t m (note that s is not part of the type). As a result, you get the coverage condition failure as described.
This is very unfortunate, because that means you also cannot have tagged effects like ...
class Monad m => TaggedState tag s m | m tag -> s where
get :: m s
put :: s -> m ()... which would improve type inference and disambiguation of effects.
But I am not an expert in all of this, so maybe there is a solution, but I just don't see it.
I’m going to close this issue, as it no longer makes sense under the rewrite, as effects are not typeclasses anymore. You might be able to get what you want under the new implementation by defining a custom typeclass (with functional dependencies) on the type-level list of effects, with :< as a superclass, but I haven’t tried it myself.
Even though this is closed, I imagine the "solution" will be to implement new type classes with FDs (per effect that needs FDs), have a superclass constraint of requiring :<, but we probably need to have a play and see if that works
Yes, that is what I just suggested.
Great, everyone's on the same page then!