Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Functional dependencies? #5

Open
johnsonwj opened this issue Nov 26, 2019 · 1 comment
Open

Functional dependencies? #5

johnsonwj opened this issue Nov 26, 2019 · 1 comment

Comments

@johnsonwj
Copy link

@johnsonwj johnsonwj commented Nov 26, 2019

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!!

@johnsonwj

This comment has been minimized.

Copy link
Author

@johnsonwj johnsonwj commented Nov 27, 2019

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!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
1 participant
You can’t perform that action at this time.