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

No type inference in some cases #31

Closed
k0ral opened this Issue Jan 8, 2015 · 4 comments

Comments

Projects
None yet
3 participants
@k0ral
Copy link

k0ral commented Jan 8, 2015

When using ext-eff, I find I have to add type annotations more than I'd like
For example (with GHC 7.8.4, ext-eff 1.9.0.1):

{-# LANGUAGE ScopedTypeVariables #-}

import Control.Eff.Reader.Lazy
import Data.Functor

-- f can be fed with anything showable, notably Int
f :: (Show a) => a -> ()
f _ = ()

-- g1 fails to compile
g1 :: (Member (Reader Int) r) => Eff r Bool
g1 = do
  f <$> ask
  return True

-- g2 fails to compile
g2 :: (Member (Reader Int) r) => Eff r Bool
g2 = do
  f <$> (ask :: Eff r Int)
  return True

-- g3 compiles
g3 :: (Member (Reader Int) r) => Eff r Bool
g3 = do
  (f :: Int -> ()) <$> ask
  return True

It looks to me that the g1 implementation has all the necessary information for GHC to infer that I'm asking for an Int. Strangely enough, type annotating ask doesn't work either.
I'm not sure whether this is an issue in extensible-effects or if it is inherent to GHC's type inference. Can you assist ?

For information, the build errors are the following:

  • for g1:
Could not deduce (Show a0) arising from a use of ‘f’
    from the context (Member (Reader Int) r)
      bound by the type signature for
                 g1 :: Member (Reader Int) r => Eff r Bool
    The type variable ‘a0’ is ambiguous
    Note: there are several potential instances:
      instance Show Control.Exception.Base.NestedAtomically
        -- Defined in ‘Control.Exception.Base’
      instance Show Control.Exception.Base.NoMethodError
        -- Defined in ‘Control.Exception.Base’
      instance Show Control.Exception.Base.NonTermination
        -- Defined in ‘Control.Exception.Base’
      ...plus 241 others
    In the first argument of ‘(<$>)’, namely ‘f’

Overlapping instances for Member (Reader a0) r
      arising from a use of ‘ask’
    Matching givens (or their superclasses):
      (Member (Reader Int) r)
        bound by the type signature for
                   g1 :: Member (Reader Int) r => Eff r Bool
    Matching instances:
      instance extensible-effects-1.9.0.1:Data.OpenUnion.Internal.OpenUnion2.Member'
                 t r
               ~ 'True =>
               Member t r
        -- Defined in ‘extensible-effects-1.9.0.1:Data.OpenUnion.Internal.OpenUnion2’
    (The choice depends on the instantiation of ‘r, a0’)
    In the second argument of ‘(<$>)’, namely ‘ask’
  • for g2:
Could not deduce (extensible-effects-1.9.0.1:Data.OpenUnion.Internal.OpenUnion2.Member'
                        (Reader Int) r1
                      ~ 'True)
    from the context (Member (Reader Int) r)
      bound by the type signature for
                 g2 :: Member (Reader Int) r => Eff r Bool
    In the second argument of ‘(<$>)’, namely ‘(ask :: Eff r Int)’

@suhailshergill suhailshergill self-assigned this Jan 15, 2015

@suhailshergill

This comment has been minimized.

Copy link
Owner

suhailshergill commented May 10, 2015

@k0ral the issue regarding the extra type annotations manifests itself in simpler examples as well. eg.

import qualified Control.Monad.Reader as CR
import Control.Eff.Reader.Lazy

-- the below compiles as expected
i1 :: CR.Reader Int Bool
i1 = do
  _ <- CR.ask
  return True

-- h1 doesn't compile
h1 :: (Member (LazyR.Reader Int) r) => Eff r Bool
h1 = do
  _ <- LazyR.ask
  return True

the above is a tradeoff of extensible-effects. specifically (and as is mentioned at the end of section 4.1 in the paper), the interface which is exposed in this library is one which favours extensibility at the cost of some more type annotations. take into consideration what the type annotation of h1 states. it states that a Reader Int type of effect is present, but it makes no mention of what else too might be present in r. as such the type of ask is inherently ambiguous. this is also related to why, in their current form, functions like LazyR.ask etc can't be grouped in a typeclass (see the README).

that being said, it is entirely possible to give up this extensibility and recover the benefit of having fewer type annotations. see ExtMTL.hs for examples. if you would like to see that functionality exposed and supported as part of the extensible-effects library, please open another issue or reopen this one.

and, apologies for the delay in getting back.

@fosskers

This comment has been minimized.

Copy link

fosskers commented May 16, 2015

I'm seeing a similar problem, perhaps you could clarify. Here's the final part of some E-E testing I'm doing:

data Dilithium = Dilithium

-- | Why can't the type of the State value be inferred?                                                                                                        
engage :: (Member (State [Dilithium]) r, Member (Exc String) r) => Eff r ()
engage = get >>= \(ds :: [Dilithium]) -> do
  if length ds < 5
     then throwExc "We're short on Dilithium, Cap'n!"
     else modify (drop 5 :: [Dilithium] -> [Dilithium])

loadCrystals :: Member (State [Dilithium]) r => [Dilithium] -> Eff r ()
loadCrystals = modify . (++)

captLog :: Member (Writer String) r => String -> Eff r ()
captLog s = tell $ "Captain's Log: " ++ s

voyage :: ( Member (Writer String) r
          , Member (State [Dilithium]) r
          , Member (Exc String) r
      ) => Eff r ()
voyage = do
  captLog "Time for a cosmic adventure!"
  captLog "Need to fill the tanks."
  loadCrystals . take 18 $ repeat Dilithium
  captLog "Engage!"
  engage >> engage >> engage >> engage
  captLog "We made it to our destination."

-- | Doesn't compile.                                                                                                                                          
vt :: Either String ()
vt = snd $ run $ evalState [] $ runMonoidWriter $ runExc voyage

vt doesn't compile, giving:

extensible-effects/Eff.hs:144:58-63: Couldn't match type ‘extensible-effects-1.9.2.2:Data.OpenUnion.Internal.OpenUnion2.Member' …                              
                           (Writer String) (Writer a0 :> (State [t0] :> Data.Void.Void))’                                                                      
                   with ‘'True’                                                                                                                                
    The type variables ‘a0’, ‘t0’ are ambiguous                                                                                                                
    In the first argument of ‘runExc’, namely ‘voyage’                                                                                                         
    In the second argument of ‘($)’, namely ‘runExc voyage’                                                                                                    
    In the second argument of ‘($)’, namely                                                                                                                    
      ‘runMonoidWriter $ runExc voyage’                                                                                                                        
Compilation failed.

What exactly does this error mean?

@fosskers

This comment has been minimized.

Copy link

fosskers commented May 16, 2015

This seems to have fixed it:

vt :: Either String ()
vt = snd $ run $ evalState ([] :: [Dilithium]) $ runWriter (++) "" $ runExc voyage
@suhailshergill

This comment has been minimized.

Copy link
Owner

suhailshergill commented May 16, 2015

the type of state value can't be inferred because of the open world
assumption that the extensible effects implementation makes. it's this
which allows us to not unnecessarily constrain what other type of effects
may be present as well. specifically, nowhere do you specify that the state
effect is unique and that dilithium is the only type of state being
handled.

On Sat, May 16, 2015, 05:01 Colin Woodbury notifications@github.com wrote:

This seems to have fixed it:

vt :: Either String ()
vt = snd $ run $ evalState ([] :: [Dilithium]) $ runWriter (++) "" $ runExc voyage


Reply to this email directly or view it on GitHub
#31 (comment)
.

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