RE: fundeps for extended Monad definition
Hello! Simon Peyton-Jones wrote:
class C a b | a -> b where {}
instance C Int Int where {}
f1 :: (forall b. (C Int b) => Int -> b) f1 x = undefined
Indeed, this gives an error message Cannot unify the type-signature variable `b' with the type `Int' Expected type: Int Inferred type: b The reason, which is thoroughly explained in Simon Peyton-Jones' message, is that the given type signature is wrong: it should read f1 :: (exists b. (C Int b) => Int -> b) Alas, 'exists' is not an allowed type quantifier. Not explicitly that is. We can get 'exists' if we use the permitted 'forall' in a negative position (aka in an existential type). The following code
class C a b | a -> b where {}
instance C Int Int where {}
newtype M a = M (forall b.(C a b) => b) f :: Int -> M Int f x = M undefined
typechecks in both Haskell compilers. Hal Daume's original example works as well:
newtype MM2 m a = MM2 (forall mb.(Monad2 m a mb) => mb)
class Monad2 m a ma | m a -> ma, ma -> m a where return2 :: a -> ma bind2 :: ma -> (a -> (MM2 m a)) -> (MM2 m a) unused :: m a -> () unused = \_ -> ()
instance Monad2 [] a [a] where bind2 = error "urk"
Again, it typechecks both in Hugs and GHC.
The reason, which is thoroughly explained in Simon Peyton-Jones' message, is that the given type signature is wrong: it should read f1 :: (exists b. (C Int b) => Int -> b)
Right. Simon pointed out that this is a pretty useless function, but not entirely so, since the result of it is not of type 'forall b. b', but rather of 'forall b. C Int b => b'. Thus, if the C class has a function which takes a 'b' as an argument, then this value does have use.
Hal Daume's original example works as well:
newtype MM2 m a = MM2 (forall mb.(Monad2 m a mb) => mb)
class Monad2 m a ma | m a -> ma, ma -> m a where return2 :: a -> ma bind2 :: ma -> (a -> (MM2 m a)) -> (MM2 m a) unused :: m a -> () unused = \_ -> ()
This wasn't quite my original example. The type of bind2 needs to be:
bind2 :: ma -> (a -> (MM2 m b)) -> (MM2 m b)
Which does typecheck. However, you cannot seem to write instances of it: instance Monad2 [] a [a] where return2 x = [x] bind2 l f = MM2 (concatMap (unmm2 . f) l) where unmm2 (MM2 mb) = mb yields our friend "cannot unify mb with [b]", both in hugs and ghc.
Hello! It seems we can truly implement Monad2 without pushing the envelope too far. The solution and a few tests are given below. In contrast to the previous approach, here we lift the type variables rather than bury them. The principle is to bring the type logic programming at the level of classes and instances but avoid putting them at the level of their members.
class TwoMonadific m a ma | m a -> ma, ma -> m a where unused :: m a -> () unused = undefined
instance TwoMonadific [] a [a]
instance TwoMonadific Maybe a (Maybe a)
class (TwoMonadific m a ma, TwoMonadific m b mb) => Monad2 m a b ma mb where return2 :: a -> ma bind2 :: ma -> (a -> mb) -> mb
instance Monad2 [] a b [a] [b] where return2 x = [x] bind2 l f = concatMap f l
instance Monad2 Maybe a b (Maybe a) (Maybe b) where return2 x = Just x bind2 Nothing f = Nothing bind2 (Just x) f = f x
test1 = (return2 5) `bind2` (\n -> [1..n]) `bind2` (\n -> [1..n])
test2 = (return2 5) `bind2` Just `bind2` Just
*Main> test1 [1,1,2,1,2,3,1,2,3,4,1,2,3,4,5] *Main> test2 Just 5
It all works in GHC. Hugs complaints about return2: ERROR "/tmp/b.hs":11 - Ambiguous type signature in class declaration *** ambiguous type : Monad2 a b c d e => b -> d *** assigned to : return2 My version of Hugs isn't up-to-date though.
participants (2)
-
Hal Daume III -
oleg＠pobox.com