Ambigous instance resolution in Haskell
Introduction and example use case
Hello! I've got a problem in Haskell. Let's consider following code
class PolyMonad m1 m2 m3 | m1 m2 -> m3 where
polyBind :: m1 a -> (a -> m2 b) -> m3 b
which just declares a poly monad binding. A good example use case scenario would be:
newtype Pure a = Pure { fromPure :: a } deriving (Show)
instance PolyMonad Pure Pure Pure where
polyBind a f = f (fromPure a)
instance PolyMonad Pure IO IO where
polyBind a f = f (fromPure a)
instance PolyMonad IO Pure IO where
polyBind a f = (fromPure . f) <$> a
instance PolyMonad IO IO IO where
polyBind a f = a >>= f
and using it with -XRebindableSyntax like so:
test = do
Pure 5
print "hello"
Pure ()
but we can do much more with it - this was only a test to show you an example case.
The problem
Lets consider a little more complex usage. I want to write a polymonad-like class, which will not always output m3 b , but in some specific cases it will output m3 (X b) for a specific X . For simplicity, lets assume we want to output m3 (X b) ONLY when either m1 or m2 was IO .
It seems we cannot do it right now in Haskell without losing flexibility. I need the following functions to compile without adding any type informations (the Haskell code is a generated one):
tst1 x = x `polyBind` (_ -> Pure 0)
tst2 = (Pure 1) `polyBind` (_ -> Pure 0)
tst3 x y = x `polyBind` (_ -> y `polyBind` (_ -> Pure 0))
Anyway these functions compile well using the PolyMonad class.
Fundep attempt to solve the problem
One of the attempts could be:
class PolyMonad2 m1 m2 m3 b | m1 m2 b -> out where
polyBind2 :: m1 a -> (a -> m2 b) -> out
and of course we can easily write all the necessary instances, like:
instance PolyMonad2 Pure Pure b (Pure b) where
polyBind2 a f = f (fromPure a)
instance PolyMonad2 Pure IO b (IO (X b)) where
polyBind2 a f = fmap X $ f (fromPure a)
-- ...
but our test functions will not compile when using polyBind2 instead of polyBind . The first function ( tst1 x = x polyBind2 (_ -> Pure 0) ) outputs a compilation error:
Could not deduce (PolyMonad2 m1 Pure b0 out)
arising from the ambiguity check for ‘tst1’
from the context (PolyMonad2 m1 Pure b out, Num b)
bound by the inferred type for ‘tst1’:
(PolyMonad2 m1 Pure b out, Num b) => m1 a -> out
at /tmp/Problem.hs:51:1-37
The type variable ‘b0’ is ambiguous
When checking that ‘tst1’
has the inferred type ‘forall (m1 :: * -> *) b out a.
(PolyMonad2 m1 Pure b out, Num b) =>
m1 a -> out’
Probable cause: the inferred type is ambiguous
Closed type families attempt to solve the problem
A slightly better way would be to use closed type families here, like:
class PolyMonad3 m1 m2 where
polyBind3 :: m1 a -> (a -> m2 b) -> OutputOf m1 m2 b
type family OutputOf m1 m2 a where
OutputOf Pure Pure a = Pure a
OutputOf x y a = Pure (X a)
but then when trying to compile the tst1 function ( tst1 x = x polyBind3 (_ -> Pure 0) ) we get another compile time error:
Could not deduce (OutputOf m1 Pure b0 ~ OutputOf m1 Pure b)
from the context (PolyMonad3 m1 Pure, Num b)
bound by the inferred type for ‘tst1’:
(PolyMonad3 m1 Pure, Num b) => m1 a -> OutputOf m1 Pure b
at /tmp/Problem.hs:59:1-37
NB: ‘OutputOf’ is a type function, and may not be injective
The type variable ‘b0’ is ambiguous
Expected type: m1 a -> OutputOf m1 Pure b
Actual type: m1 a -> OutputOf m1 Pure b0
When checking that ‘tst1’
has the inferred type ‘forall (m1 :: * -> *) a b.
(PolyMonad3 m1 Pure, Num b) =>
m1 a -> OutputOf m1 Pure b’
Probable cause: the inferred type is ambiguous
A hacky attempt to do it around
I've found another solution, but hacky and in the end not working. But it is very interesting one. Lets consider following type class:
class PolyMonad4 m1 m2 b out | m1 m2 b -> out, out -> b where
polyBind4 :: m1 a -> (a -> m2 b) -> out
Of course the functional dependency out -> b is just wrong, because we cannot define such instances like:
instance PolyMonad4 Pure IO b (IO (X b)) where
polyBind4 a f = fmap X $ f (fromPure a)
instance PolyMonad4 IO IO b (IO b) where
polyBind4 = undefined
but lets play with it and declare them so (using -XUndecidableInstances ):
instance out~(Pure b) => PolyMonad4 Pure Pure b out where
polyBind4 a f = f (fromPure a)
instance out~(IO(X b)) => PolyMonad4 Pure IO b out where
polyBind4 a f = fmap X $ f (fromPure a)
instance out~(IO b) => PolyMonad4 IO IO b out where
polyBind4 = undefined
instance out~(IO(X b)) => PolyMonad4 IO Pure b out where
polyBind4 = undefined
What's funny, some of our test functions DOES compile and work, namely:
tst1' x = x `polyBind4` (_ -> Pure 0)
tst2' = (Pure 1) `polyBind4` (_ -> Pure 0)
but this one not:
tst3' x y = x `polyBind4` (_ -> y `polyBind4` (_ -> Pure 0))
resulting in compile time error:
Could not deduce (PolyMonad4 m3 Pure b0 (m20 b))
arising from the ambiguity check for ‘tst3'’
from the context (PolyMonad4 m3 Pure b1 (m2 b),
PolyMonad4 m1 m2 b out,
Num b1)
bound by the inferred type for ‘tst3'’:
(PolyMonad4 m3 Pure b1 (m2 b), PolyMonad4 m1 m2 b out, Num b1) =>
m1 a -> m3 a1 -> out
at /tmp/Problem.hs:104:1-62
The type variables ‘m20’, ‘b0’ are ambiguous
When checking that ‘tst3'’
has the inferred type ‘forall (m1 :: * -> *)
(m2 :: * -> *)
b
out
a
(m3 :: * -> *)
b1
a1.
(PolyMonad4 m3 Pure b1 (m2 b), PolyMonad4 m1 m2 b out, Num b1) =>
m1 a -> m3 a1 -> out’
Probable cause: the inferred type is ambiguous
Even more hacky attempt using newtype wrapping
I told it is even more hacky, because it leads us to use -XIncoherentInstances , which are Just (Pure evil) . One of the ideas could be of course to write newtype wrapper:
newtype XWrapper m a = XWrapper (m (X (a)))
and some utils to unpack it:
class UnpackWrapper a b | a -> b where
unpackWrapper :: a -> b
instance UnpackWrapper (XWrapper m a) (m (X a)) where
unpackWrapper (XWrapper a) = a
instance UnpackWrapper (Pure a) (Pure a) where
unpackWrapper = id
instance UnpackWrapper (IO a) (IO a) where
unpackWrapper = id
now we can easly declare following instances:
instance PolyMonad Pure Pure Pure
instance PolyMonad Pure IO (XWrapper IO)
instance PolyMonad IO Pure (XWrapper IO)
instance PolyMonad IO IO IO
but again, we cannot run our tests when combining the bind and unwrap functions:
polyBindUnwrap a f = unpackWrapper $ polyBind a f
the test functions fail to compile again. We can mess here with some -XIncoherentInstances (see the code listing on the end), but I did not get any ok results so far.
The final question
Is this a problem which cannot be done using current GHC Haskell implementation?
Full code listing
Here is a full code listing, which can be run in GHC >= 7.8:
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
import Control.Applicative
class PolyMonad m1 m2 m3 | m1 m2 -> m3 where
polyBind :: m1 a -> (a -> m2 b) -> m3 b
----------------------------------------------------------------------
-- Some utils
----------------------------------------------------------------------
newtype Pure a = Pure { fromPure :: a } deriving (Show)
newtype X a = X { fromX :: a } deriving (Show)
main = return ()
----------------------------------------------------------------------
-- Example use cases
----------------------------------------------------------------------
instance PolyMonad Pure Pure Pure where
polyBind a f = f (fromPure a)
instance PolyMonad Pure IO IO where
polyBind a f = f (fromPure a)
instance PolyMonad IO Pure IO where
polyBind a f = (fromPure . f) <$> a
instance PolyMonad IO IO IO where
polyBind a f = a >>= f
-- works when using rebindable syntax
--test = do
-- Pure 5
-- print "hello"
-- Pure ()
tst1 x = x `polyBind` (_ -> Pure 0)
tst2 = (Pure 1) `polyBind` (_ -> Pure 0)
tst3 x y = x `polyBind` (_ -> y `polyBind` (_ -> Pure 0))
----------------------------------------------------------------------
-- First attempt to solve the problem
----------------------------------------------------------------------
class PolyMonad2 m1 m2 b out | m1 m2 b -> out where
polyBind2 :: m1 a -> (a -> m2 b) -> out
instance PolyMonad2 Pure Pure b (Pure b) where
polyBind2 a f = f (fromPure a)
instance PolyMonad2 Pure IO b (IO (X b)) where
polyBind2 a f = fmap X $ f (fromPure a)
-- ...
-- tst1 x = x `polyBind2` (_ -> Pure 0) -- does NOT compile
----------------------------------------------------------------------
-- Second attempt to solve the problem
----------------------------------------------------------------------
class PolyMonad3 m1 m2 where
polyBind3 :: m1 a -> (a -> m2 b) -> OutputOf m1 m2 b
type family OutputOf m1 m2 a where
OutputOf Pure Pure a = Pure a
OutputOf x y a = Pure (X a)
-- tst1 x = x `polyBind3` (_ -> Pure 0) -- does NOT compile
----------------------------------------------------------------------
-- Third attempt to solve the problem
----------------------------------------------------------------------
class PolyMonad4 m1 m2 b out | m1 m2 b -> out, out -> b where
polyBind4 :: m1 a -> (a -> m2 b) -> out
instance out~(Pure b) => PolyMonad4 Pure Pure b out where
polyBind4 a f = f (fromPure a)
instance out~(IO(X b)) => PolyMonad4 Pure IO b out where
polyBind4 a f = fmap X $ f (fromPure a)
instance out~(IO b) => PolyMonad4 IO IO b out where
polyBind4 = undefined
instance out~(IO(X b)) => PolyMonad4 IO Pure b out where
polyBind4 = undefined
tst1' x = x `polyBind4` (_ -> Pure 0)
tst2' = (Pure 1) `polyBind4` (_ -> Pure 0)
--tst3' x y = x `polyBind4` (_ -> y `polyBind4` (_ -> Pure 0)) -- does NOT compile
----------------------------------------------------------------------
-- Fourth attempt to solve the problem
----------------------------------------------------------------------
class PolyMonad6 m1 m2 m3 | m1 m2 -> m3 where
polyBind6 :: m1 a -> (a -> m2 b) -> m3 b
newtype XWrapper m a = XWrapper (m (X (a)))
class UnpackWrapper a b | a -> b where
unpackWrapper :: a -> b
instance UnpackWrapper (XWrapper m a) (m (X a)) where
unpackWrapper (XWrapper a) = a
instance UnpackWrapper (Pure a) (Pure a) where
unpackWrapper = id
instance UnpackWrapper (IO a) (IO a) where
unpackWrapper = id
--instance (a1~a2, out~(m a2)) => UnpackWrapper (m a1) out where
-- unpackWrapper = id
--{-# LANGUAGE OverlappingInstances #-}
--{-# LANGUAGE IncoherentInstances #-}
instance PolyMonad6 Pure Pure Pure where
polyBind6 = undefined
instance PolyMonad6 Pure IO (XWrapper IO) where
polyBind6 = undefined
instance PolyMonad6 IO Pure (XWrapper IO) where
polyBind6 = undefined
instance PolyMonad6 IO IO IO where
polyBind6 = undefined
--polyBind6' a f = unpackWrapper $ polyBind6 a f
--tst1'' x = x `polyBind6'` (_ -> Pure 0)
--tst2'' = (Pure 1) `polyBind4` (_ -> Pure 0)
--tst3'' x y = x `polyBind4` (_ -> y `polyBind4` (_ -> Pure 0)) -- does NOT compile
I don't think this question hinges on injective type families.
The injective type families bit is mentioned in the error message around the closed type family OutputOf . But, that function really is not injective -- the second equation for it allows for any x and y . GHC likes to remind users about the fact that it does not do injectivity analysis for type families, but sometimes (like here), this warning is not helpful.
Instead, the problems you're encountering all seem to stem from overloaded numbers. When you say Pure 0 , GHC correctly infers the type Num a => Pure a . The problem is that the type-level features you're accessing (type class resolution, functional dependencies, type families) care very much what specific choice is made for a here. For example, it's quite possible that any one of your approaches behaves differently for Int than it does for Integer . (For example, you could have differing instances of PolyMonad2 or extra equations in OutputOf .)
The solution to all of this might be to use RebindableSyntax and define fromInteger to be monomorphic, thus fixing the numeric type and avoiding the hassle.
I believe the fundamental difference is that here:
class PolyMonad m1 m2 m3 | m1 m2 -> m3 where
polyBind :: m1 a -> (a -> m2 b) -> m3 b
The b is fully polymorphic; it's not a parameter to the type class, so the instance can be selected and the functional dependency applied to determine m3 from m1 and m2 independently of b . It also appears in two places; if the type inferencer knows the result type or the type of the function passed to polyBind , then it can sufficiently determine b . And a type like Num b => b will happily "flow through" many applications of polyBind until it's used in a place that fixes a concrete type. Although I think it may be just the monomorphism restriction defaulting the type that saves you from an ambiguous type variable error in this case (exactly what it was designed to do).
Whereas here:
class PolyMonad2 m1 m2 m3 b | m1 m2 b -> out where
polyBind2 :: m1 a -> (a -> m2 b) -> out
b appears as a type class parameter. If we're trying to infer what out is, we need to fully determine b before we can select an instance. And there's no reason for b to bear any particular relation to the structure of the type out (or rather, that relationship can be different for each individual instance, which is after all what you're trying to achieve), so it's not possible to "follow the b through" a chain of polyBind2 calls unless you've fully resolved all of the instances.
And if b is a polymorphic number Num b => b and out is constrained by its use to be of the form Num c => mc (for some type constructor m ), there's no reason that the c and the b have to be the same Num instance. So in a chained series of polyBind2 calls operating on numbers, every intermediate result could be using a different Num instance, and without knowing any of them there's no way to select the correct PolyMonad2 instances that do unify the b with something in out . Type defaulting only applies if all the constraints on the variable are numeric prelude classes, but here the b is involved in the constraint PolyMonad2 m1 m2 m3 b , so it can't be defaulted (which is probably a good thing, since exactly what type you choose could affect which instance is used and dramatically change the program behaviour; it's only the numeric classes that are known to be "approximations" of each other, so that if the program is ambiguous about which instance to use then it's semi-reasonable to just arbitrarily pick one rather than complain about the ambiguity).
The same really goes for any method for determining out from m1 , m2 , and b as far as I know, whether it's functional dependencies, type families, or something else. I'm not sure how to actually resolve that issue here though, without providing more type annotations.
上一篇: Agda中的类型类的实例）
下一篇: Haskell中的恶意实例解析