Why does Djinn fail to realize common monadic functions?

Question

I recently stumbled across Djinn and was briefly playing around with it to try to see whether it would be useful in my everyday coding workflow. I was excited to see that Djinn had monads and tried to see whether it might be able to find some cool functions.

Djinn did in fact work some wonders. The type signature of the initially (at least to me) unintuitive function >>= (>>=) is Monad m => ((a -> m b) -> m a) -> (a -> m b) -> m b. Djinn was able to immediately demystify this by stating

Djinn> f ? Monad m => ((a -> m b) -> m a) -> (a -> m b) -> m b
f :: (Monad m) => ((a -> m b) -> m a) -> (a -> m b) -> m b
f a b = a b >>= b

Unfortunately, Djinn can't seem to find other standard functions on monads, despite knowing about the Monad typeclass.

• join (which should be join = (>>= id) or in Djinn's more verbose syntax join a = a >>= (\x -> x))

  Djinn> join ? Monad m => m (m a) -> m a
  -- join cannot be realized.
  

• liftM (which should be liftM f = (>>= (return . f)) or in Djinn's more verbose syntax liftM a b = b >>= (\x -> return (a x)))

  Djinn> liftM ? Monad m => (a -> b) -> m a -> m b
  -- liftM cannot be realized.
  

• Even the basic return :: Monad m => m a -> m (m a) cannot be found by Djinn or return :: Monad m => (a, b) -> m (a, b).

  Djinn> f ? Monad m => (a, b) -> m (a, b)
  -- f cannot be realized.
  

Djinn knows how to use \ to construct anonymous functions so why is this the case?

My rough suspicion is that perhaps Djinn has a simplistic notion of typeclass and somehow treats m a as "fixed" so that m (a, b) is not seen as a case of m a, but I have no idea how to make that any more concrete than its current hand-wavy form or whether that intuition is correct.

Answer 1

Supporting type classes properly looks a lot like supporting rank-2 types; compare:

join :: Monad m
     => m (m a) -> m a

vs:

join :: (forall a. a -> m a)
     -> (forall a b. m a -> (a -> m b) -> m b)
     -> m (m a) -> m a

Unfortunately, the techniques Djinn uses don't handle rank-2 types at all. If you float the foralls so that Djinn can process it, suddenly what you get instead are concrete choices:

join :: (b -> m b)
     -> (m c -> (c -> m d) -> m d)
     -> m (m a) -> m a

which looks a lot less like you could implement it! If you tell Djinn which instantiations to use, it does a lot better, of course.

join :: (b -> m b)
     -> (m (m a) -> (m a -> m a) -> m a)
     -> m (m a) -> m a

For this one, Djinn will give the right implementation. ...but then, that's cheating.